diff options
Diffstat (limited to 'html/Kit')
| -rw-r--r-- | html/Kit/.htaccess | 1 | ||||
| -rw-r--r-- | html/Kit/Makefile | 16 | ||||
| -rw-r--r-- | html/Kit/docs/commentary.pdf | bin | 87700 -> 0 bytes | |||
| -rw-r--r-- | html/Kit/docs/uitp03.pdf | bin | 242284 -> 0 bytes | |||
| -rw-r--r-- | html/Kit/dtd/pgip.dtd | 593 | ||||
| -rw-r--r-- | html/Kit/dtd/pgip.rnc | 411 | ||||
| -rw-r--r-- | html/Kit/dtd/pgml.dtd | 120 | ||||
| -rw-r--r-- | html/Kit/dtd/pgml.rnc | 71 |
8 files changed, 0 insertions, 1212 deletions
diff --git a/html/Kit/.htaccess b/html/Kit/.htaccess deleted file mode 100644 index c22265e7..00000000 --- a/html/Kit/.htaccess +++ /dev/null @@ -1 +0,0 @@ -# Options -Indexes diff --git a/html/Kit/Makefile b/html/Kit/Makefile deleted file mode 100644 index 3a4e7591..00000000 --- a/html/Kit/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -# -# Update exported Kit files from PG Kit repository. -# [interim] -# - -.PHONY: update - -CVSROOT=:pserver:da@cvs.inf.ed.ac.uk:/disk/cvs/proofgen - -# checkout in temp dir because otherwise CVS complains of working dir checkout -update: - mkdir kittmp - cvs -d ${CVSROOT} export -kv -D today -d kittmp kitwebfiles - (cd kittmp; tar -c . | (cd ..; tar -xp)) - rm -rf kittmp - cvs commit -m"Updated from Kit repo" diff --git a/html/Kit/docs/commentary.pdf b/html/Kit/docs/commentary.pdf Binary files differdeleted file mode 100644 index 1fe871f5..00000000 --- a/html/Kit/docs/commentary.pdf +++ /dev/null diff --git a/html/Kit/docs/uitp03.pdf b/html/Kit/docs/uitp03.pdf Binary files differdeleted file mode 100644 index ebcae29c..00000000 --- a/html/Kit/docs/uitp03.pdf +++ /dev/null diff --git a/html/Kit/dtd/pgip.dtd b/html/Kit/dtd/pgip.dtd deleted file mode 100644 index 8210331d..00000000 --- a/html/Kit/dtd/pgip.dtd +++ /dev/null @@ -1,593 +0,0 @@ -<?xml encoding="UTF-8"?> - -<!-- - -RELAX NG Schema for PGIP, the Proof General Interface Protocol - -Authors: David Aspinall, LFCS, University of Edinburgh - Christoph Lueth, University of Bremen - -Version: pgip.dtd,v 1.27 2003/09/23 23:17:18 da Exp - -Status: Experimental. -For additional commentary, see the Proof General Kit white paper, -available from http://www.proofgeneral.org/kit - -Advertised version: 1.0 - ---> - -<!ENTITY % pgml SYSTEM "pgml.dtd"> -%pgml; - -<!-- include PGML grammar --> - -<!-- ========== PGIP MESSAGES ========== --> - -<!-- complete construction of the currently open theory --> - -<!ENTITY % improperfilecmd "aborttheory|retracttheory|openfile|closefile - |abortfile|loadfile|changecwd"> - -<!ENTITY % properfilecmd "opentheory|closetheory"> - -<!-- a "literate" comment: text processed by prover, but no sidefx --> - -<!ENTITY % improperproofcmd "undostep|abortgoal|forget|restoregoal"> - -<!ENTITY % properproofcmd "opengoal|proofstep|closegoal|postponegoal - |giveupgoal|comment|litcomment"> - -<!-- change prover's working directory (or load path) for files --> - -<!ENTITY % fileinfomsg "informfileloaded|informfileretracted"> - -<!-- ========== GENERAL PROVER OUTPUT/RESPONSES ========== --> - -<!ENTITY % proveroutput "ready|cleardisplay|normalresponse|errorresponse - |scriptinsert|metainforesponse|parseresult - |unparseresult"> - -<!-- ========== INTERFACE CONFIGURATION ========== --> - -<!ENTITY % kitconfig "usespgip|usespgml|pgmlconfig|proverinfo|hasprefs - |prefval|guiconfig|setids|addids|delids|idvalue - |menuadd|menudel"> - -<!-- ========== THEORY/FILE HANDLING COMMANDS ========== --> - -<!ENTITY % filecmd "%properfilecmd;|%improperfilecmd;"> - -<!-- ========= PROOF CONTEXT/ETC COMMANDS =========== --> - -<!ENTITY % proofctxt "askids|showid|setid|parsescript|unparsecmds - |showproofstate|showctxt|searchtheorems - |setlinewidth|viewdoc"> - -<!-- data values --> - -<!-- ========== PROOF CONTROL COMMANDS ========== --> - -<!ENTITY % proofcmd "%properproofcmd;|%improperproofcmd;"> - -<!-- text is arg to "viewdoc" --> - -<!-- ========== PROVER CONTROL ========== --> - -<!ENTITY % provercontrol "proverinit|proverexit|startquiet|stopquiet - |pgmlsymbolson|pgmlsymbolsoff"> - -<!-- information messages concerning --> - -<!-- ========== PROVER CONFIGURATION ========== --> - -<!ENTITY % proverconfig "askpgip|askpgml|askconfig|askprefs|setpref - |getpref"> - -<!-- issue a file command --> - -<!ENTITY % kitmsg "%kitconfig;|%proveroutput;|%fileinfomsg;"> - -<!-- for a message sent TO proof general --> - -<!ENTITY % provermsg "%proverconfig;|%provercontrol;|%proofcmd; - |%proofctxt;|%filecmd;"> - -<!-- -pgips is the type of a log between -two components. ---> - -<!ELEMENT pgip (%provermsg;|%kitmsg;)> - -<!-- or an interface message --> - -<!ELEMENT pgips (pgip)+> - -<!-- sequence number of this message --> - -<!ENTITY % pgip_class "pa|pg"> - -<!ATTLIST pgip - origin CDATA #IMPLIED - id CDATA #REQUIRED - class (%pgip_class;) #REQUIRED - refseq CDATA #IMPLIED - refid CDATA #IMPLIED - seq CDATA #REQUIRED> - -<!-- please tell me this preference value --> - -<!ENTITY % name_attr " - name CDATA #REQUIRED"> - -<!-- identifiers must be XML tokens --> - -<!ENTITY % prefcat_attr " - prefcategory CDATA #REQUIRED"> - -<!-- -e.g. "expert", "internal", etc. -could be used for tabs in dialog ---> - -<!ELEMENT askpgip EMPTY> - -<!ELEMENT askpgml EMPTY> - -<!ELEMENT askconfig EMPTY> - -<!ELEMENT askprefs EMPTY> -<!ATTLIST askprefs - prefcategory CDATA #IMPLIED> - -<!ELEMENT setpref (#PCDATA)> -<!ATTLIST setpref - %name_attr; - prefcategory CDATA #IMPLIED> - -<!ELEMENT getpref EMPTY> -<!ATTLIST getpref - %name_attr; - prefcategory CDATA #IMPLIED> - -<!-- remove a menu entry --> - -<!-- version reporting --> - -<!ENTITY % version_attr " - version CDATA #REQUIRED"> - -<!ELEMENT usespgml EMPTY> -<!ATTLIST usespgml - %version_attr;> - -<!ELEMENT usespgip EMPTY> -<!ATTLIST usespgip - %version_attr;> - -<!-- PGML configuration --> - -<!ELEMENT pgmlconfig (%pgmlconfigure;)+> - -<!-- -Types for config settings: corresponding data values should conform -to representation for corresponding XML Schema 1.0 Datatypes. -(This representation is verbose but helps for error checking later) ---> - -<!ENTITY % pgiptype "pgipbool|pgipint|pgipstring|pgipchoice"> - -<!ELEMENT pgipbool EMPTY> - -<!ELEMENT pgipint EMPTY> -<!ATTLIST pgipint - min CDATA #IMPLIED - max CDATA #IMPLIED> - -<!ENTITY % min_attr " - min CDATA #REQUIRED"> - -<!ENTITY % max_attr " - max CDATA #REQUIRED"> - -<!ELEMENT pgipstring EMPTY> - -<!ELEMENT pgipchoice (pgipchoiceitem)+> - -<!ELEMENT pgipchoiceitem (#PCDATA)> - -<!ELEMENT icon (#PCDATA)> - -<!-- image data for an icon --> - -<!-- preferences --> - -<!ENTITY % default_attr " - default CDATA #REQUIRED"> - -<!ENTITY % descr_attr " - descr CDATA #REQUIRED"> - -<!-- -icons for preference recommended size: 32x32 -top level preferences: may be used in dialog for preference setting -object preferences: may be used as an "emblem" to decorate -object icon (boolean preferences with default false, only) ---> - -<!ELEMENT haspref (icon?,(%pgiptype;))> -<!ATTLIST haspref - %name_attr; - descr CDATA #IMPLIED - default CDATA #IMPLIED> - -<!ELEMENT hasprefs (haspref)*> -<!ATTLIST hasprefs - prefcategory CDATA #IMPLIED> - -<!ELEMENT prefval (#PCDATA)> -<!ATTLIST prefval - %name_attr;> - -<!-- menu items (incomplete) --> - -<!ENTITY % path_attr " - path CDATA #REQUIRED"> - -<!ELEMENT menuadd (#PCDATA)> -<!ATTLIST menuadd - path CDATA #IMPLIED - name CDATA #IMPLIED> - -<!ELEMENT menudel (#PCDATA)> -<!ATTLIST menudel - path CDATA #IMPLIED - name CDATA #IMPLIED> - -<!-- -GUI configuration information: objects, types, and operations -NB: the following object types have a fixed interpretation -in PGIP: "comment", "thm", "theory", "file" ---> - -<!ELEMENT guiconfig (objtype*,opn*)> - -<!ELEMENT objtype (icon?,hasprefs?,contains*)> -<!ATTLIST objtype - %name_attr; - descr CDATA #IMPLIED> - -<!ENTITY % objtype_attr " - objtype CDATA #REQUIRED"> - -<!-- the name of an objtype --> - -<!ELEMENT contains EMPTY> -<!ATTLIST contains - %objtype_attr;> - -<!-- source types: a space separated list --> - -<!ENTITY % optrg "optrg?"> - -<!-- --> - -<!ELEMENT opn (inputform?,opsrc,(%optrg;),opcmd)> -<!ATTLIST opn - %name_attr;> - -<!ELEMENT optrg (#PCDATA)> - -<!ELEMENT opsrc (#PCDATA)> - -<!-- single target type, empty for proofstate --> - -<!ELEMENT opcmd (#PCDATA)> - -<!-- prover command, with printf-style "%1"-args --> - -<!-- interactive operations - require some input --> - -<!ELEMENT inputform (field)+> - -<!-- -a field has a PGIP config type (int, string, bool, choice(c1...cn)) -and a name; under that name, it will be substituted into the command -Ex. field name=number opcmd="rtac %1 %number" ---> - -<!ELEMENT field ((%pgiptype;),prompt)> -<!ATTLIST field - %name_attr;> - -<!ELEMENT prompt (#PCDATA)> - -<!-- -identifier tables: these list known items of particular objtype. -Might be used for completion or menu selection, and inspection. -May have a nested structure (but objtypes do not). ---> - -<!ELEMENT setids (idtable)> - -<!-- (with an empty idtable, clear table) --> - -<!ELEMENT addids (idtable)> - -<!ELEMENT delids (idtable)> - -<!ENTITY % displaytext "(#PCDATA|pgml)*"> - -<!-- give value of some identifier (response to showid) --> - -<!ELEMENT idvalue %displaytext;> -<!ATTLIST idvalue - %name_attr; - %objtype_attr;> - -<!ELEMENT idtable (identifier|idtable)*> -<!ATTLIST idtable - %objtype_attr;> - -<!ELEMENT identifier (#PCDATA)> - -<!-- -prover information: -name, description, version, homepage, -welcome message, docs available ---> - -<!ELEMENT proverinfo (welcomemsg?,icon?,helpdoc*)> -<!ATTLIST proverinfo - %name_attr; - descr CDATA #IMPLIED - version CDATA #IMPLIED - url CDATA #IMPLIED> - -<!ELEMENT welcomemsg (#PCDATA)> - -<!ENTITY % url_attr " - url CDATA #REQUIRED"> - -<!-- FIXME: schema for URL? --> - -<!-- -helpdoc: advertise availability of some documentation, given a canonical -name, textual description, and URL or viewdoc argument. - ---> - -<!ELEMENT helpdoc (#PCDATA)> -<!ATTLIST helpdoc - %name_attr; - %descr_attr; - url CDATA #IMPLIED> - -<!-- deactivate use of symbols in PGML output --> - -<!ELEMENT proverinit EMPTY> - -<!ELEMENT proverexit EMPTY> - -<!ELEMENT startquiet EMPTY> - -<!ELEMENT stopquiet EMPTY> - -<!ELEMENT pgmlsymbolson EMPTY> - -<!ELEMENT pgmlsymbolsoff EMPTY> - -<!-- result of a <unparsecmds> request (see later) --> - -<!ELEMENT ready EMPTY> - -<!ENTITY % displayarea "message|display"> - -<!-- the main display area (goals buffer) --> - -<!ELEMENT cleardisplay EMPTY> -<!ATTLIST cleardisplay - area (%displayarea;|all) #REQUIRED> - -<!-- grammar for displayed text --> - -<!ELEMENT normalresponse %displaytext;> -<!ATTLIST normalresponse - area (%displayarea;) #REQUIRED - category CDATA #IMPLIED - urgent (y) #IMPLIED> - -<!ENTITY % fatality "nonfatal|fatal|panic"> - -<!-- degree of errors --> - -<!ELEMENT errorresponse %displaytext;> -<!ATTLIST errorresponse - fatality (%fatality;) #REQUIRED - location CDATA #IMPLIED - locationline CDATA #IMPLIED - locationcolumn CDATA #IMPLIED> - -<!ELEMENT scriptinsert (#PCDATA)> - -<!-- metainformation is an extensible place to put system-specific information --> - -<!ELEMENT value (#PCDATA)> -<!ATTLIST value - name CDATA #IMPLIED> - -<!-- generic value holder --> - -<!ELEMENT metainforesponse (value)*> -<!ATTLIST metainforesponse - infotype CDATA #REQUIRED> - -<!-- re-open previously postponed proof, outdating dependent theorems --> - -<!ENTITY % thmname_attr " - thmname CDATA #REQUIRED"> - -<!-- theorem names --> - -<!ENTITY % aname_attr " - aname CDATA #REQUIRED"> - -<!-- anchors in proof text --> - -<!ELEMENT opengoal (#PCDATA)> -<!ATTLIST opengoal - %thmname_attr;> - -<!-- text is theorem to be proved --> - -<!ELEMENT proofstep (#PCDATA)> -<!ATTLIST proofstep - aname CDATA #IMPLIED> - -<!-- text is proof command --> - -<!ELEMENT undostep EMPTY> - -<!ELEMENT closegoal EMPTY> -<!ATTLIST closegoal - %thmname_attr;> - -<!ELEMENT abortgoal EMPTY> -<!ATTLIST abortgoal - %thmname_attr;> - -<!ELEMENT giveupgoal EMPTY> -<!ATTLIST giveupgoal - %thmname_attr;> - -<!ELEMENT postponegoal EMPTY> -<!ATTLIST postponegoal - %thmname_attr;> - -<!ELEMENT forget EMPTY> -<!ATTLIST forget - thyname CDATA #IMPLIED - aname CDATA #IMPLIED> - -<!ELEMENT restoregoal EMPTY> -<!ATTLIST restoregoal - %thmname_attr;> - -<!ELEMENT comment (#PCDATA)> - -<!ELEMENT litcomment (#PCDATA)> - -<!-- request some on-line help (prover-specific arg) --> - -<!ENTITY % thyname_attr " - thyname CDATA #REQUIRED"> - -<!-- theory name --> - -<!ELEMENT askids EMPTY> -<!ATTLIST askids - thyname CDATA #IMPLIED - %objtype_attr;> - -<!ELEMENT showid EMPTY> -<!ATTLIST showid - thyname CDATA #IMPLIED - %objtype_attr; - %name_attr;> - -<!ELEMENT setid (setpref*,obvalue)> -<!ATTLIST setid - %name_attr; - %objtype_attr;> - -<!ELEMENT obvalue (#PCDATA)> - -<!-- text constructed with opcmds --> - -<!-- -NB: parse/unparsing needs only be supported for "proper" proof commands, -which may appear in proof texts. ---> - -<!ENTITY % properscriptcmd "%properproofcmd;|%properfilecmd;|setid"> - -<!ELEMENT parsescript (#PCDATA)> - -<!ELEMENT parseresult (%properscriptcmd;)*> - -<!ELEMENT unparsecmds (%properscriptcmd;)*> - -<!ELEMENT unparseresult (#PCDATA)> - -<!ELEMENT showproofstate EMPTY> - -<!ELEMENT showctxt EMPTY> - -<!ELEMENT searchtheorems (#PCDATA)> - -<!ELEMENT setlinewidth (#PCDATA)> - -<!ELEMENT viewdoc (#PCDATA)> - -<!-- prover informs interface a particular file is outdated --> - -<!-- -Below, url_attr will often be a file URL. -We assume for now that the prover and interface are running on same -filesystem ---> - -<!ATTLIST changecwd - dir CDATA #REQUIRED> - -<!-- Unix directory name --> - -<!ELEMENT opentheory (#PCDATA)> -<!ATTLIST opentheory - %thyname_attr;> - -<!ELEMENT closetheory EMPTY> -<!ATTLIST closetheory - %thyname_attr;> - -<!ELEMENT aborttheory EMPTY> -<!ATTLIST aborttheory - %thyname_attr;> - -<!ELEMENT retracttheory EMPTY> -<!ATTLIST retracttheory - %thyname_attr;> - -<!-- -FIXME: maybe add a command to ask prover for the file corresponding -to some theory (prover searches it's search path / cwd). ---> - -<!ELEMENT loadfile EMPTY> -<!ATTLIST loadfile - %url_attr;> - -<!ELEMENT openfile EMPTY> -<!ATTLIST openfile - %url_attr;> - -<!ELEMENT closefile EMPTY> -<!ATTLIST closefile - %url_attr;> - -<!ELEMENT abortfile EMPTY> -<!ATTLIST abortfile - %url_attr;> - -<!ELEMENT changecwd EMPTY> - -<!ELEMENT informfileloaded EMPTY> -<!ATTLIST informfileloaded - %thyname_attr; - %url_attr;> - -<!ELEMENT informfileretracted EMPTY> -<!ATTLIST informfileretracted - %thyname_attr; - %url_attr;> diff --git a/html/Kit/dtd/pgip.rnc b/html/Kit/dtd/pgip.rnc deleted file mode 100644 index 0555dc21..00000000 --- a/html/Kit/dtd/pgip.rnc +++ /dev/null @@ -1,411 +0,0 @@ -# -# RELAX NG Schema for PGIP, the Proof General Interface Protocol -# -# Authors: David Aspinall, LFCS, University of Edinburgh -# Christoph Lueth, University of Bremen -# -# Version: pgip.rnc,v 1.37 2003/09/25 09:11:49 da Exp -# -# Status: Experimental. -# For additional commentary, see the Proof General Kit white paper, -# available from http://www.proofgeneral.org/kit -# -# Advertised version: 1.0 -# - - - -include "pgml.rnc" # include PGML grammar - -# ========== PGIP MESSAGES ========== - -start = pgip | pgips # pgips is the type of a log between - # two components. - -pgip = element pgip { # A PGIP packet contains: - pgip_attrs, # attributes with header information; - (provermsg # either a message sent TO the prover, - | kitmsg)} # or an interface message - -pgips = element pgips { pgip+ } - -pgip_attrs = - attribute origin { text }?, # name of sending PGIP component - attribute id { text }, # session identifier for component process - attribute class { pgip_class }, # general categorization of message - attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to - attribute refid { text }?, # message id this message responds to - attribute seq { xsd:positiveInteger } # sequence number of this message - - -pgip_class = "pa" # for a message sent TO the proof assistant - | "pg" # for a message sent TO proof general - -provermsg = - proverconfig # query Prover configuration, triggering interface configuration - | provercontrol # control some aspect of Prover - | proofcmd # issue a proof command - | proofctxt # issue a context command - | filecmd # issue a file command - -kitmsg = - kitconfig # messages to configure the interface - | proveroutput # output messages from the prover, usually display in interface - | fileinfomsg # information messages concerning - - - - -# ========== PROVER CONFIGURATION ========== - -proverconfig = - askpgip # what version of PGIP do you support? - | askpgml # what version of PGML do you support? - | askconfig # tell me about objects and operations - | askprefs # what preference settings do you offer? - | setpref # please set this preference value - | getpref # please tell me this preference value - -name_attr = attribute name { token } # identifiers must be XML tokens - - -prefcat_attr = attribute prefcategory { text} # e.g. "expert", "internal", etc. - # could be used for tabs in dialog - -askpgip = element askpgip { empty } -askpgml = element askpgml { empty } -askconfig = element askconfig { empty } -askprefs = element askprefs { prefcat_attr? } -setpref = element setpref { name_attr, prefcat_attr?, text } -getpref = element getpref { name_attr, prefcat_attr? } - - - -# ========== INTERFACE CONFIGURATION ========== - -kitconfig = - usespgip # I support PGIP, version .. - | usespgml # I support PGML, version .. - | pgmlconfig # configure PGML symbols - | proverinfo # Report assistant information - | hasprefs # I have preference settings ... - | prefval # the current value of a preference is - | guiconfig # configure the following object types and operations - | setids # inform the interface about some known objects - | addids # add some known identifiers - | delids # retract some known identifers - | idvalue # display the value of some identifier - | menuadd # add a menu entry - | menudel # remove a menu entry - -# version reporting -version_attr = attribute version { text } -usespgml = element usespgml { version_attr } -usespgip = element usespgip { version_attr } - -# PGML configuration -pgmlconfig = element pgmlconfig { pgmlconfigure+ } - -# Types for config settings: corresponding data values should conform -# to representation for corresponding XML Schema 1.0 Datatypes. -# (This representation is verbose but helps for error checking later) - -pgiptype = pgipbool | pgipint | pgipstring | pgipchoice -pgipbool = element pgipbool { empty } - -pgipint = element pgipint { min_attr?, max_attr?, empty } -min_attr = attribute min { xsd:integer } -max_attr = attribute max { xsd:integer } -pgipstring = element pgipstring { empty } -pgipchoice = element pgipchoice { pgipchoiceitem+ } -pgipchoiceitem = element pgipchoiceitem { text } - -icon = element icon { xsd:base64Binary } # image data for an icon - -# preferences -default_attr = attribute default { text } -descr_attr = attribute descr { text } - -# icons for preference recommended size: 32x32 -# top level preferences: may be used in dialog for preference setting -# object preferences: may be used as an "emblem" to decorate -# object icon (boolean preferences with default false, only) -haspref = element haspref { - name_attr, descr_attr?, - default_attr?, icon?, - pgiptype -} - -hasprefs = element hasprefs { prefcat_attr?, haspref* } - -prefval = element prefval { name_attr, text } - -# menu items (incomplete) -path_attr = attribute path { text } - -menuadd = element menuadd { path_attr?, name_attr?, text } -menudel = element menudel { path_attr?, name_attr?, text } - - -# GUI configuration information: objects, types, and operations -# NB: the following object types have a fixed interpretation -# in PGIP: "comment", "thm", "theory", "file" - -guiconfig = - element guiconfig { objtype*, opn* } - -objtype = element objtype { name_attr, descr_attr?, icon?, hasprefs?, contains* } - -objtype_attr = attribute objtype { token } # the name of an objtype -contains = element contains { objtype_attr, empty } # - -opn = element opn { name_attr, inputform?, opsrc, optrg, opcmd } - -opsrc = element opsrc { list { token* } } # source types: a space separated list -optrg = element optrg { token }? # single target type, empty for proofstate -opcmd = element opcmd { text } # prover command, with printf-style "%1"-args - -# interactive operations - require some input -inputform = element inputform { field+ } - -# a field has a PGIP config type (int, string, bool, choice(c1...cn)) -# and a name; under that name, it will be substituted into the command -# Ex. field name=number opcmd="rtac %1 %number" - -field = element field { - name_attr, pgiptype, - element prompt { text } -} - -# identifier tables: these list known items of particular objtype. -# Might be used for completion or menu selection, and inspection. -# May have a nested structure (but objtypes do not). - -setids = element setids { idtable } # (with an empty idtable, clear table) -addids = element addids { idtable } -delids = element delids { idtable } - -# give value of some identifier (response to showid) -idvalue = element idvalue - { name_attr, objtype_attr, displaytext } - -idtable = element idtable { objtype_attr, (identifier | idtable)* } -identifier = element identifier { token } - -# prover information: -# name, description, version, homepage, -# welcome message, docs available -proverinfo = element proverinfo - { name_attr, descr_attr?, version_attr?, url_attr?, - welcomemsg?, icon?, helpdoc* } -welcomemsg = element welcomemsg { text } -url_attr = attribute url { text } # FIXME: schema for URL? - -# helpdoc: advertise availability of some documentation, given a canonical -# name, textual description, and URL or viewdoc argument. -# -helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, text } # text is arg to "viewdoc" - - -# ========== PROVER CONTROL ========== - -provercontrol = - proverinit # reset prover to its initial state - | proverexit # exit prover - | startquiet # stop prover sending proof state displays, non-urgent messages - | stopquiet # turn on normal proof state & message displays - | pgmlsymbolson # activate use of symbols in PGML output (input always understood) - | pgmlsymbolsoff # deactivate use of symbols in PGML output - -proverinit = element proverinit { empty } -proverexit = element proverexit { empty } -startquiet = element startquiet { empty } -stopquiet = element stopquiet { empty } -pgmlsymbolson = element pgmlsymbolson { empty } -pgmlsymbolsoff = element pgmlsymbolsoff { empty } - - -# ========== GENERAL PROVER OUTPUT/RESPONSES ========== - -proveroutput = - ready # prover is ready for input - | cleardisplay # prover requests a display area to be cleared - | proofstate # prover outputs the proof state - | normalresponse # prover outputs some display - | errorresponse # prover indicates an error condition, with error message - | scriptinsert # some text to insert literally into the proof script - | metainforesponse # prover outputs some other meta-information to interface - | parseresult # result of a <parsescript> request (see later) - | unparseresult # result of a <unparsecmds> request (see later) - -ready = element ready { empty } - -displayarea = "message" # the message area (response buffer) - | "display" # the main display area (goals buffer) - -cleardisplay = - element cleardisplay { - attribute area { - displayarea | "all" } } - - -displaytext = (text | pgml)* # grammar for displayed text - -proofstate = - element proofstate { displaytext } - -normalresponse = - element normalresponse { - attribute area { displayarea }, - attribute category { text }?, # optional extra category (e.g. tracing/debug) - attribute urgent { "y" }?, # indication that message must be displayed - displaytext -} - -fatality = "nonfatal" | "fatal" | "panic" # degree of errors - -errorresponse = - element errorresponse { - attribute fatality { fatality }, - attribute location { text }?, - attribute locationline { xsd:positiveInteger }?, - attribute locationcolumn { xsd:positiveInteger }?, - displaytext - } - -scriptinsert = element scriptinsert { text } - - -# metainformation is an extensible place to put system-specific information - -value = element value { name_attr?, text } # generic value holder - -metainforesponse = - element metainforesponse { - attribute infotype { text }, # categorization of data - value* } # data values - - -# ========== PROOF CONTROL COMMANDS ========== - -proofcmd = - properproofcmd | improperproofcmd - -properproofcmd = - opengoal # open a goal in ambient context - | proofstep # a specific proof command (perhaps configured via opcmd) - | closegoal # complete & close current open proof (succeeds iff goal proven) - | giveupgoal # close current open proof, record as proof obl'n (sorry) - | postponegoal # close current open proof, retaining attempt in script (oops) - | comment # an ordinary comment: text ignored by prover - | litcomment # a "literate" comment: text processed by prover, but no sidefx - -improperproofcmd = - undostep # undo the last proof step issued in currently open goal - | abortgoal # give up on current open proof, close proof state, discard history - | forget # forget a theorem (or named target), outdating dependent theorems - | restoregoal # re-open previously postponed proof, outdating dependent theorems - -thmname_attr = attribute thmname { text } # theorem names -aname_attr = attribute aname { text } # anchors in proof text - -opengoal = element opengoal { thmname_attr, text } # text is theorem to be proved -proofstep = element proofstep { aname_attr?, text } # text is proof command -undostep = element undostep { empty } - -closegoal = element closegoal { empty } -abortgoal = element abortgoal { empty } -giveupgoal = element giveupgoal { empty } -postponegoal = element postponegoal { empty } -forget = element forget { thyname_attr?, aname_attr? } -restoregoal = element restoregoal { thmname_attr } -comment = element comment { text } -litcomment = element litcomment { text } - - -# ========= PROOF CONTEXT/ETC COMMANDS =========== - -proofctxt = - askids # please tell me about identifiers (given objtype in a theory) - | showid # print value of an object - | bindid # extend current context with identifer assignment - | parsescript # parse a raw proof script into proofcmds - | unparsecmds # unprase proofcmds into raw proof script - | showproofstate # (re)display proof state (empty if outside a proof) - | showctxt # show proof context - | searchtheorems # search for theorems (prover-specific arguments) - | setlinewidth # set line width for printing - | viewdoc # request some on-line help (prover-specific arg) - -thyname_attr = attribute thyname { text } # theory name - -askids = element askids { thyname_attr?, objtype_attr } - -showid = element showid { thyname_attr?, objtype_attr, name_attr } -bindid = element setid { name_attr, objtype_attr, setpref*, objval } -objval = element obvalue { text } # text constructed with opcmds - - -# NB: parse/unparsing needs only be supported for "proper" proof commands, -# which may appear in proof texts. - -properscriptcmd = properproofcmd | properfilecmd | bindid - -parsescript = element parsescript { text } -parseresult = element parseresult { properscriptcmd* } - -unparsecmds = element unparsecmds { properscriptcmd* } -unparseresult = element unparseresult { text } - -showproofstate = element showproofstate { empty } -showctxt = element showctxt { empty } -searchtheorems = element searchtheorems { text } -setlinewidth = element setlinewidth { xsd:positiveInteger } -viewdoc = element viewdoc { text } - - -# ========== THEORY/FILE HANDLING COMMANDS ========== - -filecmd = - properfilecmd | improperfilecmd - -properfilecmd = - opentheory # begin construction of a new theory. - | closetheory # complete construction of the currently open theory - -improperfilecmd = - aborttheory # abort currently open theory - | retracttheory # retract a named theory - | openfile # lock a file for constructing a proof text - | closefile # unlock a file, suggesting it has been processed - | abortfile # unlock a file, suggesting it hasn't been processed - | loadfile # load a file possibly containing theory definition(s) - | changecwd # change prover's working directory (or load path) for files - -fileinfomsg = - informfileloaded # prover informs interface a particular file is loaded - | informfileretracted # prover informs interface a particular file is outdated - -# Below, url_attr will often be a file URL. -# We assume for now that the prover and interface are running on same -# filesystem - -dir_attr = attribute dir { text } # Unix directory name - -opentheory = element opentheory { thyname_attr, text } -closetheory = element closetheory { empty } -aborttheory = element aborttheory { empty } -retracttheory = element retracttheory { thyname_attr } - -# FIXME: maybe add a command to ask prover for the file corresponding -# to some theory (prover searches it's search path / cwd). -loadfile = element loadfile { url_attr } -openfile = element openfile { url_attr } -closefile = element closefile { empty } -abortfile = element abortfile { empty } -changecwd = element changecwd { dir_attr } - -informfileloaded = - element informfileloaded { thyname_attr, url_attr } -informfileretracted = - element informfileretracted { thyname_attr, url_attr } diff --git a/html/Kit/dtd/pgml.dtd b/html/Kit/dtd/pgml.dtd deleted file mode 100644 index fbdd9f7d..00000000 --- a/html/Kit/dtd/pgml.dtd +++ /dev/null @@ -1,120 +0,0 @@ -<?xml encoding="UTF-8"?> - -<!-- - -RELAX NG Schema for PGML, the Proof General Markup Language - -Authors: David Aspinall, LFCS, University of Edinburgh - Christoph Lueth, University of Bremen -Version: pgml.dtd,v 1.12 2003/09/23 23:17:18 da Exp - -Status: Complete but experimental version. - -For additional commentary, see the Proof General Kit white paper, -available from http://www.proofgeneral.org/kit - -Advertised version: 1.0 - ---> - -<!ENTITY % pgml_version_attr " - version NMTOKEN #REQUIRED"> - -<!ELEMENT pgml (statedisplay|termdisplay|information|warning|error)*> -<!ATTLIST pgml - version NMTOKEN #IMPLIED> - -<!ENTITY % nonactionitem "term|type|atom|sym"> - -<!ENTITY % termitem "action|%nonactionitem;"> - -<!ENTITY % pgml_name_attr " - name CDATA #REQUIRED"> - -<!ENTITY % kind_attr " - kind CDATA #REQUIRED"> - -<!ENTITY % systemid_attr " - systemid CDATA #REQUIRED"> - -<!ELEMENT statedisplay (#PCDATA|%termitem;|statepart)*> -<!ATTLIST statedisplay - name CDATA #IMPLIED - kind CDATA #IMPLIED - systemid CDATA #IMPLIED> - -<!ENTITY % pgmltext "(#PCDATA|%termitem;)*"> - -<!ELEMENT information %pgmltext;> -<!ATTLIST information - name CDATA #IMPLIED - kind CDATA #IMPLIED> - -<!ELEMENT warning %pgmltext;> -<!ATTLIST warning - name CDATA #IMPLIED - kind CDATA #IMPLIED> - -<!ELEMENT error %pgmltext;> -<!ATTLIST error - name CDATA #IMPLIED - kind CDATA #IMPLIED> - -<!ELEMENT statepart %pgmltext;> -<!ATTLIST statepart - name CDATA #IMPLIED - kind CDATA #IMPLIED> - -<!ELEMENT termdisplay %pgmltext;> -<!ATTLIST termdisplay - name CDATA #IMPLIED - kind CDATA #IMPLIED> - -<!ENTITY % pos_attr " - pos CDATA #REQUIRED"> - -<!ELEMENT term %pgmltext;> -<!ATTLIST term - pos CDATA #IMPLIED - kind CDATA #IMPLIED> - -<!-- maybe combine this with term and add extra attr to term? --> - -<!ELEMENT type %pgmltext;> -<!ATTLIST type - kind CDATA #IMPLIED> - -<!ELEMENT action (#PCDATA|%nonactionitem;)*> -<!ATTLIST action - kind CDATA #IMPLIED> - -<!ENTITY % fullname_attr " - fullname CDATA #REQUIRED"> - -<!ELEMENT atom (#PCDATA)> -<!ATTLIST atom - kind CDATA #IMPLIED - fullname CDATA #IMPLIED> - -<!ENTITY % symname_attr " - name CDATA #REQUIRED"> - -<!ELEMENT sym EMPTY> -<!ATTLIST sym - %symname_attr;> - -<!-- configuring PGML --> - -<!ENTITY % pgmlconfigure "symconfig"> - -<!-- inform symbol support (I/O) for given sym --> - -<!ENTITY % asciialt " - alt CDATA #REQUIRED"> - -<!-- understanding of ASCII alt for given sym --> - -<!ELEMENT symconfig EMPTY> -<!ATTLIST symconfig - %symname_attr; - alt CDATA #IMPLIED> diff --git a/html/Kit/dtd/pgml.rnc b/html/Kit/dtd/pgml.rnc deleted file mode 100644 index 4e5c8053..00000000 --- a/html/Kit/dtd/pgml.rnc +++ /dev/null @@ -1,71 +0,0 @@ -# -# RELAX NG Schema for PGML, the Proof General Markup Language -# -# Authors: David Aspinall, LFCS, University of Edinburgh -# Christoph Lueth, University of Bremen -# Version: pgml.rnc,v 1.5 2003/09/23 23:12:47 da Exp -# -# Status: Complete but experimental version. -# -# For additional commentary, see the Proof General Kit white paper, -# available from http://www.proofgeneral.org/kit -# -# Advertised version: 1.0 -# - -pgml_version_attr = attribute version { xsd:NMTOKEN } - -pgml = - element pgml { - pgml_version_attr?, - (statedisplay | termdisplay | information | warning | error)* - } - -termitem = action | nonactionitem -nonactionitem = term | pgmltype | atom | sym - -pgml_name_attr = attribute name { text } - -kind_attr = attribute kind { text } -systemid_attr = attribute systemid { text } - -statedisplay = - element statedisplay { - pgml_name_attr?, kind_attr?, systemid_attr?, - (text | termitem | statepart)* - } - -pgmltext = (text | termitem)* - -information = - element information { pgml_name_attr?, kind_attr?, pgmltext } - -warning = element warning { pgml_name_attr?, kind_attr?, pgmltext } -error = element error { pgml_name_attr?, kind_attr?, pgmltext } -statepart = element statepart { pgml_name_attr?, kind_attr?, pgmltext } -termdisplay = element termdisplay { pgml_name_attr?, kind_attr?, pgmltext } - -pos_attr = attribute pos { text } - -term = element term { pos_attr?, kind_attr?, pgmltext } - -# maybe combine this with term and add extra attr to term? -pgmltype = element type { kind_attr?, pgmltext } - -action = element action { kind_attr?, (text | nonactionitem)* } - -fullname_attr = attribute fullname { text } -atom = element atom { kind_attr?, fullname_attr?, text } - - -## Symbols - -symname_attr = attribute name { text } -sym = element sym { symname_attr } - -# configuring PGML - -pgmlconfigure = symconfig # inform symbol support (I/O) for given sym -asciialt = attribute alt { text } # understanding of ASCII alt for given sym - -symconfig = element symconfig { symname_attr, asciialt? } |