# HG changeset patch
# User aspinall
# Date 1128094084 -7200
# Node ID 863cdca5c77a9aca84034a0a718cc4d4c5f3a4c5
# Parent  e6948d8f5f7387857137f380fa7eb621797b7103
Schema files (for information, and validating pgip_isar.xml)

diff -r e6948d8f5f73 -r 863cdca5c77a lib/ProofGeneral/pgml.rnc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/ProofGeneral/pgml.rnc	Fri Sep 30 17:28:04 2005 +0200
@@ -0,0 +1,80 @@
+# 
+# RELAX NG Schema for PGML, the Proof General Markup Language
+# 
+# Authors:  David Aspinall, LFCS, University of Edinburgh       
+#           Christoph Lueth, University of Bremen       
+# Version: $Id$    
+# 
+# Status:  Complete, prototype.
+# 
+# For additional commentary, see accompanying commentary document
+# (available at http://proofgeneral.inf.ed.ac.uk/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_mixed    = text | termitem | statepart 
+
+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?,
+    pgml_mixed*
+  }
+
+pgmltext    = element 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
+##
+## Element sym can be rendered in three alternative ways, 
+## in descending preference order:
+##
+## 1) the PGML symbol given by the name attribute
+## 2) the text content of the SYM element, if non-empty
+## 3) one of the previously configured text alternatives advertised
+##    by the component who produced this output.
+##
+symname_attr = attribute name { token }        # names must be [a-zA-Z][a-zA-Z0-9]+
+sym          = element sym { symname_attr, text }
+
+
+pgmlconfigure = symconfig              # inform symbol support (I/O) for given sym
+
+textalt = attribute alt { text }       # text alternative for given sym
+
+symconfig = element symconfig { symname_attr, textalt* }
diff -r e6948d8f5f73 -r 863cdca5c77a lib/ProofGeneral/schemas.xml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/ProofGeneral/schemas.xml	Fri Sep 30 17:28:04 2005 +0200
@@ -0,0 +1,5 @@
+<?xml version="1.0"?>
+<locatingRules xmlns="http://thaiopensource.com/ns/locating-rules/1.0">
+  <uri resource="pgip_isar.xml" uri="pgip.rnc"/>
+  <uri resource="pgip_isar.xml" typeId="RELAX NG"/>
+</locatingRules>