PGML

<?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: $Id: pgml.rnc,v 1.4 2003/08/25 17:25:08 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 "
  name CDATA #REQUIRED">

<!ELEMENT sym EMPTY>
<!ATTLIST sym
  %symname;>

<!-- 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;
  alt CDATA #IMPLIED>