aboutsummaryrefslogtreecommitdiff
path: root/html/Kit
diff options
context:
space:
mode:
Diffstat (limited to 'html/Kit')
-rw-r--r--html/Kit/Makefile11
-rw-r--r--html/Kit/dtd/pgip.dtd226
-rw-r--r--html/Kit/dtd/pgml.dtd75
3 files changed, 312 insertions, 0 deletions
diff --git a/html/Kit/Makefile b/html/Kit/Makefile
new file mode 100644
index 00000000..b35b720b
--- /dev/null
+++ b/html/Kit/Makefile
@@ -0,0 +1,11 @@
+#
+# Update dtds from PG Kit repository.
+#
+
+.PHONY: dtdupdate
+
+DTDTARGS=dtd/pgip.dtd dtd/pgml.dtd
+
+# checkout in temp dir because otherwise CVS complains of repo clash (fixes?)
+dtdupdate:
+ mkdir dtdtmp; cvs -d :ext:da@localssh.dcs.ed.ac.uk:/home/proofgen/src export -kv -D today -d dtdtmp Kit/dtd; mv dtdtmp/* dtd; rmdir dtdtmp; cvs commit -m"Updated from Kit repo" dtd
diff --git a/html/Kit/dtd/pgip.dtd b/html/Kit/dtd/pgip.dtd
new file mode 100644
index 00000000..2861fff2
--- /dev/null
+++ b/html/Kit/dtd/pgip.dtd
@@ -0,0 +1,226 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for PGIP, the Proof General Interface Protocol -->
+<!-- Author: David Aspinall, LFCS, University of Edinburgh -->
+<!-- Version: pgip.dtd,v 1.6 2001/09/10 19:00:42 da Exp -->
+
+<!-- Status: Incomplete. -->
+<!-- For commentary, see the Proof General Kit white paper, -->
+<!-- available from http://www.proofgeneral.org/kit -->
+
+
+<!ELEMENT pgip (%provermsg; | %kitmsg;)*>
+<!ATTLIST pgip
+ version CDATA
+ class CDATA #IMPLIED
+ origin CDATA
+ id CDATA>
+
+
+<!-- STATUS/ERROR MESSAGES -->
+<!-- ===================== -->
+
+<!ELEMENT information (#PCDATA)>
+<!ATTLIST information
+ kind CDATA #IMPLIED
+ location CDATA #IMPLIED>
+
+<!-- kind=message,urgentmessage,display -->
+
+<!ELEMENT error (#PCDATA)>
+<!ATTLIST error
+ kind CDATA #IMPLIED
+ location CDATA #IMPLIED>
+
+<!-- kind=warning,fatal,interrupt -->
+
+<!ENTITY % proverstatus "information | error">
+
+
+
+<!-- CONFIGURATION MESSAGES -->
+<!-- ====================== -->
+
+<!ENTITY % kitconfig "usespgml | haspref | prefval | idtable |
+ addid | delid | menuadd | menudel | guiconfig">
+
+<!-- This is how it should be:
+ <!ENTITY % pgml SYSTEM "pgml.dtd">
+ -->
+
+<!-- Types for config settings -->
+
+<!ELEMENT pgipbool EMPTY>
+<!ELEMENT pgipint (#PCDATA)>
+<!ELEMENT pgipstring (#PCDATA)>
+<!ELEMENT pgipchoice (pgipchoiceitem+)>
+<!ELEMENT pgipchoiceitem (#PCDATA)>
+<!ATTLIST pgipchoiceitem
+ tag CDATA #IMPLIED>
+
+<!ENTITY % pgiptype "pgipbool | pgipint | pgipstring | pgipchoice">
+
+
+<!ELEMENT usespgml EMPTY>
+<!ATTLIST usespgml
+ version CDATA #IMPLIED>
+
+<!ELEMENT haspref pgiptype>
+<!ATTLIST haspref
+ default CDATA #IMPLIED
+ class CDATA #IMPLIED>
+
+<!ELEMENT prefval (#PCDATA)>
+<!ATTLIST prefval
+ name CDATA #IMPLIED>
+
+<!ELEMENT idtable (#PCDATA)>
+<!ATTLIST idtable
+ class CDATA #IMPLIED>
+
+<!ELEMENT addid (#PCDATA)>
+<!ATTLIST addid
+ class CDATA #IMPLIED>
+
+<!ELEMENT delid (#PCDATA)>
+<!ATTLIST delid
+ class CDATA #IMPLIED>
+
+<!ELEMENT menuadd (#PCDATA)>
+<!ATTLIST menuadd
+ path CDATA #IMPLIED
+ name CDATA #IMPLIED>
+
+<!ELEMENT menudel (#PCDATA)>
+<!ATTLIST menudel
+ path CDATA #IMPLIED
+ name CDATA #IMPLIED>
+
+
+<!-- gui configuration -->
+
+<!-- the PCDATA is the icon, base64-encoded -->
+<!ELEMENT objtype (#PCDATA)>
+<!ATTLIST objtype
+ name CDATA #REQUIRED>
+
+<!ELEMENT opn (opsrc, optrg, opcmd)>
+<!ATTLIST opn
+ name CDATA #REQUIRED>
+
+<!-- source types as space-separated list; target type is a single type -->
+<!ELEMENT opsrc (#PCDATA)>
+<!ELEMENT optrg (#PCDATA)>
+<!-- the prover command, with a printf "%1"-style substitution of arguments -->
+<!ELEMENT opcmd (#PCDATA)>
+
+<!-- proof operations (no target sort) -->
+<!ELEMENT proofopn (opsrc, opcmd)>
+<!ATTLIST opn
+ name CDATA #REQUIRED>
+
+<!-- interactive operations-- require some input -->
+<!ELEMENT iopn (inputform, opsrc, optrg, opcmd)>
+<!ATTLIST iopn
+ name CDATA #REQUIRED>
+
+<!-- an input form is a list of fields -->
+<!ELEMENT inputform (field)+>
+<!-- and a field has a 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" -->
+<!-- the PCDATA is the prompt for the input field -->
+<!ELEMENT field (pgiptype)>
+<!ATTLIST field
+ type CDATA #REQUIRED
+ name CDATA #REQUIRED>
+
+
+<!ELEMENT guiconfig (objtype*, opn*, iopn*, proofopn*) >
+
+
+
+<!ENTITY % proverconfig "askpgml | askprefs | resetprefs |
+ setpref | getpref">
+
+<!ELEMENT askpgml EMPTY>
+
+<!ELEMENT askprefs EMPTY>
+<!ATTLIST askprefs
+ class CDATA #IMPLIED>
+
+<!ELEMENT resetprefs EMPTY>
+<!ATTLIST resetprefs
+ class CDATA #IMPLIED>
+
+<!ELEMENT setpref EMPTY>
+<!ATTLIST setpref
+ class CDATA #IMPLIED>
+
+<!ELEMENT getpref EMPTY>
+<!ATTLIST getpref
+ class CDATA #IMPLIED>
+
+
+
+<!-- COMMANDS -->
+<!-- ======== -->
+
+<!ELEMENT provercmd (#PCDATA)>
+
+<!ELEMENT goalcmd (#PCDATA)>
+
+<!ELEMENT undocmd EMPTY>
+
+<!ELEMENT abortcmd EMPTY>
+
+<!ELEMENT closecmd (#PCDATA)
+ goalid CDATA #REQUIRED>
+
+<!ELEMENT postponecmd (#PCDATA)
+ goalid CDATA #REQUIRED
+ thmname CDATA #REQUIRED>
+
+<!ELEMENT savecmd EMPTY>
+<!ATTLIST savecmd
+ thmname CDATA #REQUIRED>
+
+<!ELEMENT forgetcmd EMPTY>
+<!ATTLIST forgetcmd
+ thmname CDATA #REQUIRED>
+
+<!ELEMENT restorecmd EMPTY>
+<!ATTLIST restorecmd
+ goalid CDATA #REQUIRED>
+
+<!ELEMENT loadfilecmd (#PCDATA)>
+
+<!ELEMENT retractfilecmd (#PCDATA)>
+
+<!ENTITY % command "provercmd | goalcmd | undocmd | savecmd | forgetcmd |
+ closecmd | quitcmd | postponecmd | restorecmd |
+ loadfilecmd | retractfilecmd">
+
+<!-- savecmd Finishes a proof and saves a new theorem
+ closecmd Temporarily closes a proof and saves state with given id
+ postponecmd As closecmd, but saves a new theorem and
+ generates a proof obligation
+ -->
+
+
+
+
+<!-- Roots of PGIP messages -->
+
+<!-- Messages sent to PG Kit components -->
+
+<!ENTITY % kitmsg "%kitconfig | %proverstatus">
+
+<!-- Messages sent to proof assistant (class "pa") -->
+
+<!ENTITY % provermsg "proverconfig">
+
+
+
+
+<!ELEMENT br EMPTY>
diff --git a/html/Kit/dtd/pgml.dtd b/html/Kit/dtd/pgml.dtd
new file mode 100644
index 00000000..d484c100
--- /dev/null
+++ b/html/Kit/dtd/pgml.dtd
@@ -0,0 +1,75 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for PGML, the Proof General Markup Language -->
+<!-- Author: David Aspinall, LFCS, University of Edinburgh -->
+<!-- Version: pgml.dtd,v 1.6 2001/09/10 16:04:17 da Exp -->
+
+<!-- Status: Complete but experimental version. -->
+<!-- For commentary, see the Proof General Kit white paper, -->
+<!-- available from http://www.proofgeneral.org/kit -->
+
+
+<!ELEMENT pgml (statedisplay | termdisplay | information | warning | error)*>
+<!ATTLIST pgml
+ version CDATA #IMPLIED>
+
+<!ELEMENT statedisplay (statepart)*>
+<!ATTLIST statedisplay
+ systemid CDATA #IMPLIED
+ name CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!ENTITY % termitem "action | term | type | atom | sym">
+<!ENTITY % nonactionitem "term | type | atom | sym">
+
+<!ELEMENT information (#PCDATA | %termitem;)*>
+<!ATTLIST information
+ name CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!ELEMENT warning (#PCDATA | %termitem;)*>
+<!ATTLIST warning
+ name CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!ELEMENT error (#PCDATA | %termitem;)*>
+<!ATTLIST error
+ name CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!ELEMENT statepart (#PCDATA | %termitem;)*>
+<!ATTLIST statepart
+ name CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!ELEMENT termdisplay (#PCDATA | %termitem;)*>
+<!ATTLIST termdisplay
+ name CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!ELEMENT term (#PCDATA | %termitem;)*>
+<!ATTLIST term
+ pos CDATA #IMPLIED
+ kind CDATA #IMPLIED>
+
+<!-- maybe combine this with term and add extra attr to term? -->
+<!ELEMENT type (#PCDATA | %termitem;)*>
+<!ATTLIST type
+ kind CDATA #IMPLIED>
+
+<!ELEMENT action (#PCDATA | %nonactionitem;)*>
+<!ATTLIST action
+ kind CDATA #IMPLIED>
+
+<!ELEMENT atom (#PCDATA)>
+<!ATTLIST atom
+ kind CDATA #IMPLIED
+ fullname CDATA #IMPLIED>
+
+<!ELEMENT sym (#PCDATA)>
+<!ATTLIST sym
+ name CDATA #IMPLIED
+ alt CDATA #IMPLIED>
+
+<!ELEMENT br EMPTY>
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:00:45 +0000