Added kit stuff: just copies of the DTDs at the moment.

2 files changed, 184 insertions, 0 deletions

diff --git a/html/Kit/dtd/pgip.dtd b/html/Kit/dtd/pgip.dtd
new file mode 100644
index 00000000..fd3e839c
--- /dev/null
+++ b/html/Kit/dtd/pgip.dtd
@@ -0,0 +1,116 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for PGIP, the Proof General Interface Protocol		   -->
+<!-- Author:  David Aspinall, LFCS, University of Edinburgh        -->
+<!-- Version: $Id$     -->
+
+<!-- Status:  Incomplete.					   -->
+<!-- For commentary, see the Proof General Kit white paper, at     -->
+<!-- http://zermelo.dcs.ed.ac.uk/~proofgen/kit.html		   -->
+
+<!ELEMENT pgip (%provermsg; | %kitmsg;)*>
+<!ATTLIST pgip
+	    version CDATA 
+	    class   CDATA #IMPLIED
+	    origin  CDATA 
+	    id	    CDATA>
+
+<!-- Messages sent to PG Kit components -->
+
+<!ENTITY % kitmsg     "%kitconfig | %proverstatus">
+
+<!-- Messages sent to proof assistant (class "pa") -->
+
+<!ENTITY % provermsg	"proverconfig">
+
+
+<!-- STATUS/ERROR MESSAGES -->
+<!-- ===================== -->
+
+<!ENTITY % proverstatus "information | error">
+
+<!ELEMENT information (#PCDATA)>
+<!ATTLIST information
+	   kind		CDATA #IMPLIED
+	   location	CDATA>
+
+<!-- kind=message,urgentmessage,display -->
+
+<!ELEMENT error (#PCDATA)>
+<!ATTLIST error
+	   kind		CDATA #IMPLIED
+	   location	CDATA>
+
+<!-- kind=warning,fatal,interrupt -->
+
+
+
+<!-- CONFIGURATION MESSAGES -->
+<!-- ====================== -->
+
+<!ENTITY % kitconfig  "usespgml | haspref | prefval | idtable | 
+			addid | delid | menuadd | menudel">
+
+<!ELEMENT usespgml EMPTY>
+<!ATTLIST usespgml 
+	   version CDATA #IMPLIED>
+
+<!ELEMENT haspref (#PCDATA)>
+<!ATTLIST haspref 
+	   type     CDATA #IMPLIED
+	   default  CDATA
+	   class    CDATA>
+
+<!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>	   	
+	   
+	   
+<!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>
+
+
+
+
+
+<!ELEMENT br EMPTY>
diff --git a/html/Kit/dtd/pgml.dtd b/html/Kit/dtd/pgml.dtd
new file mode 100644
index 00000000..cead27bf
--- /dev/null
+++ b/html/Kit/dtd/pgml.dtd
@@ -0,0 +1,68 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for PGML, the Proof General Markup Language		   -->
+<!-- Author:  David Aspinall, LFCS, University of Edinburgh	   -->
+<!-- Status:  Complete but experimental version.		   -->
+<!-- Version: $Id$     -->
+
+<!ELEMENT pgml (statedisplay | 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 
+	   systemid CDATA #IMPLIED
+	   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>
+
+