lib/ProofGeneral/pgip.rnc

 # 
 # RELAX NG Schema for PGIP, the Proof General Interface Protocol                   
 # 
 # Authors:  David Aspinall, LFCS, University of Edinburgh       
-#           Christoph Lueth, University of Bremen       
+#           Christoph Lüth, University of Bremen       
 #
 # Version: $Id$    
 # 
 # Status:   Prototype.
 #

 #  4. Prover Configuration
 #  5. Interface Configuration
 #  6. Prover Control
 #  7. Proof script markup and proof control
 #
+#
+# ===============================================================================
+#
+# Note on datatypes.  (see e.g. http://books.xmlschemata.org/relaxng):
+#
+#  token  : any string possibly with spaces, but spaces are normalised/collapsed
+#	    (i.e. tokenised).  Same as XML Schema xs:token
+#  string : any string, whitespaces preserved.  Same as XML Schema xs:string
+#	    (NB: attributes are normalised by XML 1.0 parsers so
+#	     spaces/newlines must be quoted)
+#  text	  : text nodes/mixed content (whitespace may be lost in mixed content)
+#
+# So: attributes should usually be tokens or more restrictive; (sometimes: strings for printing)
+#     element contents may be string (preserving whitespace), token (tokenising), 
+#       or text (which may contain further nodes).
 
 # ==============================================================================
 # 0. Prelude
 # ==============================================================================
 
 include "pgml.rnc"                           # include PGML grammar
 
-name_attr = attribute name { text }          # names are user-level textual identifiers
-thyname_attr = attribute thyname { text }    # names for theories (special case of name)
-thmname_attr = attribute thmname { text }    # names for theorems (special case of name)
+name_attr = attribute name { token }         # names are user-level textual identifiers (space-collapsed)
+thyname_attr = attribute thyname { token }   # names for theories (special case of name)
+thmname_attr = attribute thmname { token }   # names for theorems (special case of name)
 
 datetime_attr = 
    attribute datetime { xsd:dateTime }       # CCYY-MM-DDHH:MM:SS plus timezone info
 url_attr  = attribute url { xsd:anyURI }     # URLs  (often as "file:///localfilename.extn")
-dir_attr  = attribute dir { text }           # Unix-style directory name (no final slash)
+dir_attr  = attribute dir { string }         # Unix-style directory name (no final slash)
 
 systemdata_attr  = 
-            attribute systemdata { text }?   # system-specific data (useful for "stateless" RPC)
-
-
-objname = string
-termobjname = string                         # (User-level) object names, semi-colon terminated
-objnames = string                            # A sequence of objnames
-
-#termobjname  = xsd:string { pattern = "[^;]+;" }  # unfortunately these declarations don't 
+            attribute systemdata { token }?   # system-specific data (useful for "stateless" RPC)
+
+objname = token	     # an identifier name (convention: any characters except semi-colon)
+objnames = token     # sequence of names in an attribute: semi-colon separated
+
+#objnames = string                            # A sequence of objnames
+#termobjname  = string { pattern = "[^;]+;" }  # unfortunately these declarations don't 
+#objnames = objname | (termobjname, objname)
 #objnames = objname+                               #  work with the RNC->DTD tool trang
 
 
 # ==============================================================================
 # 1. Top-level Messages/documents

 
 start = pgip                                 # Single message
       | pgips                                # A log of messages between components
       | displayconfig                        # displayconfig as a standalone element
       | pgipconfig                           # pgipconfig as a standalone element
+      | pgipdoc                              # A proof script document 
 
 pgip = element pgip {                        #  A PGIP packet contains:
    pgip_attrs,                               #   - attributes with header information;
    (toprovermsg | todisplaymsg |             #   - a message with one of four channel types
     fromprovermsg | fromdisplaymsg 

   }
 
 pgips = element pgips { pgip+ }
 
 pgip_attrs =
- attribute tag { text }?,                   # message tag, e.g. name of origin component (diagnostic)
- attribute id { text },                     # (unique) session id of this component 
- attribute destid { text }?,                # session id of destination component
+ attribute tag { token }?,                  # message tag, e.g. name of origin component (diagnostic)
+ attribute id { token },                    # (unique) session id of this component 
+ attribute destid { token }?,               # session id of destination component
  attribute class { pgip_class },            # general categorization of message
- attribute refid { text }?,                 # component id this message responds to (usually destid)
+ attribute refid { token }?,                # component id this message responds to (usually destid)
  attribute refseq { xsd:positiveInteger }?, # message sequence this message responds to
  attribute seq { xsd:positiveInteger }      # sequence number of this message
 
-pgip_class = "pg"      # message sent TO proof general broker
+pgip_class = "pg"      # message sent TO proof general broker (e.g. FROM proof assistant).
            | "pa"      # message sent TO the proof assistant/other component
            | "pd"      # message sent TO display/front-end components
 
 toprovermsg =          # Messages sent to the prover (class "pa"):
    proverconfig        #   query Prover configuration, triggering interface configuration

 componentspec = 
    element componentspec {
       componentid_attr,         # Unique identifier for component class
       componentname_attr,       # Textual name of component class
       componenttype,            # Type of component: prover, display, auxiliary
-      systemattrs,              # System attributes for connecting to component
+      startupattrs,		# Describing startup behaviour
+      systemattrs,              # System attributes for component
       componentconnect          # How to connect to component
    }
 
 componentid_attr   = attribute componentid   { token }
-componentname_attr = attribute componentname { text }
+componentname_attr = attribute componentname { token }
 
 componenttype = element componenttype {
      provercomponent 
    | displaycomponent 
  # | filehandlercomponent 

 
 componentconnect =
    componentsubprocess | componentsocket | connectbyproxy
 
 componentsubprocess = 
-   element syscommand { text }
+   element syscommand { string }
 componentsocket = 
-   (element host { text }, element port { text })
+   (element host { token }, element port { xsd:positiveInteger })
 connectbyproxy = 
-   (element proxy { attribute host { text }    # Host to connect to
+   (element proxy { attribute host { token }    # Host to connect to
 		  , attribute connect { 
                            "rsh" | "ssh" # Launch proxy via RSH or SSH, needs
 			                 # authentication 
                          | "server"  # connect to running proxy on given port
                          }?
-                  , attribute user { text } ? # user to connect as with RSH/SSH
-		  , attribute port { text } ? # port to connect to running proxy
+                  , attribute user { token } ? # user to connect as with RSH/SSH
+                  , attribute path { token } ? # path of pgipkit on remote
+		  , attribute port { xsd:positiveInteger } ? # port to connect to running proxy
 		  , componentconnect
 		  })
 
-systemattrs = (
-   attribute timeout { xsd:integer }?,  # timeout for communications
-   attribute sync { xsd:boolean }?,     # whether to wait for ready
-   attribute startup {		# what to do on broker startup:
+# Attributes describing when to start the component.
+startupattrs =
+  attribute startup {		# what to do on broker startup:
              "boot"   |		# always start this component (default with displays)
              "manual" |		# start manually (default with provers)
-             "ignore"		# never start this
+             "ignore"		# never start this component
              }?
-   )
+
+# System attributes describing behaviour of component. 
+systemattrs = (
+    attribute timeout { xsd:integer }?  # timeout for communications
+  , attribute sync { xsd:boolean }?     # whether to wait for ready
+  , attribute nestedgoals { xsd:boolean}? # Does prover allow nested goals?
+  )
 
 # Control commands from display to broker
 brokercontrol = 
     launchprover		# Launch a new prover
   | exitprover			# Request to terminate a running prover

 
 brokerstatus  = element brokerstatus 
                        { knownprovers, runningprovers, brokerinformation }
 
 knownprover   = element knownprover   { componentid_attr, provername }
-runningprover = element runningprover { proverid_attr, provername }
+runningprover = element runningprover { componentid_attr, proverid_attr, provername }
 
 knownprovers   = element knownprovers { knownprover* }
 runningprovers = element runningprovers { runningprover* }
-brokerinformation = element brokerinformation { text }
+brokerinformation = element brokerinformation { string }
 
 proveravailmsg  = element proveravailable { provername_attr,
                                             componentid_attr }
-newprovermsg    = element proverstarted { provername_attr, 
-		                          proverid_attr }
-                  # QUESTION: do we want  componentid_attr 
-                  # here as well, and do we want to be able to run multiple
-                  # copies of the same prover? 
+newprovermsg    = element proverstarted { proverid_attr
+					, componentid_attr
+		                        , provername_attr
+		                        }
 proverstatemsg = element proverstate { 
                        proverid_attr, provername_attr,
                        attribute proverstate {proverstate} } 
 
 proverstate    = ("ready" | "busy" | "exitus")

   | savefile			# save opened file
   | discardfile			# discard changes to opened file
 
 dispfilemsg =
     newfile			# announce creation of new file (in response to load/open)
-  | filestatus			#announce change in status of file in broker
+  | filestatus			# announce change in status of file in broker
 
 # unique identifier of loaded files
-srcid_attr = attribute srcid { text }
+srcid_attr = attribute srcid { token }
 
 loadparsefile = element loadparsefile { url_attr, proverid_attr }
-newfilewith   = element newfilewith   { url_attr, proverid_attr, text }
+newfilewith   = element newfilewith   { url_attr, proverid_attr, string }
 dispopenfile  = element dispopenfile { url_attr,
                                        proverid_attr,
                                        attribute overwrite { xsd:boolean }?}
 savefile      = element savefile { srcid_attr,     
                                    url_attr? }
 discardfile   = element discardfile { srcid_attr }
 
 newfile       = element newfile  { proverid_attr, srcid_attr, url_attr }
-filestatus    = element filestatus  { proverid_attr, srcid_attr, newstatus_attr, 
+filestatus    = element filestatus  { proverid_attr, srcid_attr, newstatus_attr, url_attr?,
 				      datetime_attr} 
 
 newstatus_attr = attribute newstatus { "saved" | "changed" | "discarded" }
 
 dispobjcmd =
     setobjstate			# request of change of state 
-  | editobj			# request edit operation of opbjects
+  | editobj			# request edit operation of objects
   | createobj			# request creation of new objects
+# Suggested May 06: probably add re-load flags instead 
+#  | reloadobjs                  # request relisting of all objects
   | inputcmd		        # process the command (generated by an input event)
   | interruptprover		# send interrupt or kill signal to prover
 
 dispobjmsg = element dispobjmsg { 
       newobj+			# new objects have been created

 	    objid_attr, 
             attribute objposition { objid } ?,
             objtype_attr ?,
             attribute objparent { objid }?,
             attribute objstate { objstate },
+	    # FIXME: would like to include metainfo here
+            # as (properscriptcmd, metainfo*) | unparseable
             (properscriptcmd | unparseable) }
 
 replaceobjs = element replaceobjs {
 	                srcid_attr,
 	                attribute replacedfrom { objid }? ,
 			attribute replacedto { objid }?,
-                        delobj*,
-                        newobj+ }
+                        delobj*,    # actually, either of delobj or 
+                        newobj* }   # newobj can be empty but not both.
 
 delobj = element delobj   { proverid_attr, srcid_attr, objid_attr }
 
 objectstate = element objstate
                        { proverid_attr, srcid_attr, objid_attr,

                   {  objid_attr, attribute newstate {objstate} }
 
 editobj = element editobj { srcid_attr ?,
 	                    attribute editfrom { objid }?,
                             attribute editto   { objid }?,
-                            text }
+                            string }
 createobj = element createobj { srcid_attr ?, 
                                 attribute objposition { objid }?, 
-                                text}
-
-inputcmd       = element inputcmd { improper_attr, text }
+                                string }
+
+# Suggested May 06: probably add re-load flags instead 
+# reloadobjs = element reloadobjs { srcid_attr }
+
+inputcmd       = element inputcmd { improper_attr, string }
 improper_attr  = attribute improper { xsd:boolean }
 
 interruptprover = element interruptprover 
                           { interruptlevel_attr, proverid_attr }
 
 interruptlevel_attr  = attribute interruptlevel { "interrupt" | "stop" | "kill" }
 
 objid_attr = attribute objid { objid } 
-objid      = text 
+objid      = token 
 
 objstate = 
   ( "unparseable" | "parsed" | "being_processed" | "processed" | "outdated" )
 
 

  | setpref			# please set this preference value 
  | getpref			# please tell me this preference value
 
 
 
-prefcat_attr = attribute prefcategory { text}   # e.g. "expert", "internal", etc.
-                                                # could be used for tabs in dialog
+prefcat_attr = attribute prefcategory { token }   # 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? }

   | idvalue			# display the value of some identifier
   | menuadd			# add a menu entry
   | menudel			# remove a menu entry
 
 # version reporting
-version_attr  = attribute version { text }
+version_attr  = attribute version { token }
 usespgml = element usespgml  { version_attr }
 usespgip = element usespgip  { version_attr 
 	                     , activecompspec
 			     }
 

 # There are some restrictions: if we start a tool, the componentid and the type must be the
 # same as initially specified.
 activecompspec =  ( componentid_attr?   # unique identifier of component class
 	          , componentname_attr? # Textual name of this component (overrides initial spec)
 		  , componenttype?      # Type of component
+		  , systemattrs         # system attributes
 		  , acceptedpgipelems?  # list of accepted elements
 		  )
 
 
 acceptedpgipelems = element acceptedpgipelems { singlepgipelem* }
 
 singlepgipelem    = element pgipelem { 
    attribute async { xsd:boolean }?,  # true if this command supported asynchronously (deflt false)
-   text }                             # (otherwise part of ready/sync stream)
+				      # (otherwise part of usual ready/sync stream)
+   attribute attributes { text }?,    # comma-separated list of supported optional attribute names
+				      # useful for: times attribute
+   text }                             # the unadorned name of the PGIP element (*not* an element)
 
 # PGML configuration
 pgmlconfig = element pgmlconfig { pgmlconfigure+ }
 
 # Types for config settings: corresponding data values should conform to canonical
-# representation for corresponding XML Schema 1.0 Datatypes.  (This representation is verbose
-# but helps for error checking later)
+# representation for corresponding XML Schema 1.0 Datatypes.  
 #
 # In detail:
+#  pgipnull   = empty
 #  pgipbool   = xsd:boolean = true | false
 #  pgipint    = xsd:integer = (-)?(0-9)+     (canonical: no leading zeroes)
-#  pgipstring = xsd:string  =  <any character sequence>
+#  pgipstring = string  =  <any non-empty character sequence>
 #  pgipchoice = cf xs:choice  = type1 | type2 | ... | typen
 
-pgiptype   = pgipbool | pgipint | pgipstring | pgipchoice | pgipconst
-pgipbool   = element pgipbool { empty }
-
-pgipint    = element pgipint  { min_attr?, max_attr?, empty }
+pgiptype   = pgipnull | pgipbool | pgipint | pgipstring | pgipchoice | pgipconst
+
+pgipnull   = element pgipnull { descr_attr?, empty }
+pgipbool   = element pgipbool { descr_attr?, empty }
+pgipint    = element pgipint  { min_attr?, max_attr?, descr_attr?, empty }
 min_attr   = attribute min { xsd:integer }
 max_attr   = attribute max { xsd:integer }
-pgipstring = element pgipstring { empty }
+pgipstring = element pgipstring { descr_attr?, empty }
+pgipconst  = element pgipconst { name_attr, descr_attr? } 
+      # FIXME: Temporary fix because Isabelle does it wrong -- should be empty }
 pgipchoice = element pgipchoice { pgiptype+ }
-pgipconst  = element pgipconst { name_attr?, text }
-
-pgipvalue  = text
+
+# Notes on pgipchoice:
+# 1. Choices must not be nested (i.e. must not contain other choices)
+# 2. The description attributes for pgipbool, pgipint, pgipstring and pgipconst
+#    are for use with pgipchoice: they can be used as a user-visible label
+#    when representing the choice to the user (e.g. in a pull-down menu).
+# 3. A pgipchoice should have an unambiguous representation as a string. That means
+#    all constants in the choice must have different names, and a choice must not
+#    contain more than one each of pgipint, pgipstring and pgipbool.
+
+pgipvalue  = string
 
 icon  = element icon { xsd:base64Binary }  # image data for an icon
 
-default_attr = attribute default { text }
-descr_attr   = attribute descr { text }
+# The default value of a preference as a string (using the unambiguous
+# conversion to string mentioned above). A string value will always be quoted
+# to distinguish it from constants or integers.
+default_attr = attribute default { token }
+
+# Description of a choice.  If multi-line, first line is short tip.
+descr_attr   = attribute descr { string }
 
 # 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)

    name_attr, descr_attr?, 
    default_attr?, icon?,
    pgiptype
 }
 
+
+
 hasprefs = element hasprefs { prefcat_attr?, haspref* }
 
 prefval = element prefval { name_attr, pgipvalue } 
 
 # menu items (incomplete, FIXME)
-path_attr = attribute path { text }
+path_attr = attribute path { token }
 
 menuadd  = element menuadd  { path_attr?, name_attr?, opn_attr? }
 menudel  = element menudel  { path_attr?, name_attr? }
 opn_attr = attribute operation { token }
 

 # basic prover information, lexical structure of files, 
 # an icon for the prover, help documents, and the 
 # objects, types, and operations for building proof commands.
 
 # NB: the following object types have a fixed interpretation 
-# in PGIP:  "comment", "theorem", "theory", "file" 
+# in PGIP:
+#        "identifier":   an identifier in the identifier syntax
+#           "comment":   an arbitrary sequence of characters
+#	    "theorem":   a theorem name or text
+#	    "theory" :   a theory name or text
+#	    "file" :     a file name
 
 displayconfig =
   element displayconfig { 
      welcomemsg?, icon?, helpdoc*, lexicalstructure*,
      objtype*, opn* }
 
-objtype = element objtype { name_attr, descr_attr?, icon?, hasprefs?, contains* }
+objtype = element objtype { name_attr, descr_attr?, icon?,  contains*, hasprefs?  }
 
 objtype_attr = attribute objtype { token }           # the name of an objtype
 contains = element contains { objtype_attr, empty }  #  a container for other objtypes
 
-opn   = element opn { name_attr, inputform?, opsrc, optrg, opcmd, improper_attr? }
-
-opsrc = element opsrc { list { token* } }  # source types: a space separated list
-optrg = element optrg { token }?           # single target type, empty for proof command
-opcmd = element opcmd { text }             # prover command, with printf-style "%1"-args
+opn = element opn { 
+   name_attr, 
+   descr_attr?,
+   inputform?,	  # FIXME: can maybe remove this?
+   opsrc*,	  # FIXME: incompat change wanted: have list of source elts, not spaces
+   optrg, 
+   opcmd, 
+   improper_attr? }
+
+opsrc = 
+   element opsrc {	  
+      name_attr?,         # %name as an alternative to %number
+      selnumber_attr?,    # explicit number for %number, the nth item selected
+      prompt_attr?,	  # prompt in form or tooltip in template
+      listwithsep_attr?,  # list of args of this type with given separator
+      list { token* } }   # source types: a space separated list
+			  # FIXME incompat change wanted: just have one source here
+			  # FIXME: need to add optional pgiptype
+
+listwithsep_attr =  attribute listwithsep { token }
+selnumber_attr =    attribute selnumber { xsd:positiveInteger }
+prompt_attr =       attribute prompt { string }
+
+optrg = 
+   element optrg { token }?           # single target type, empty for proof command
+opcmd = 
+   element opcmd { string }           # prover command, with printf-style "%1"-args
+					   #  (whitespace preserved here: literal text)
 
 # 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 }
+   element prompt { string }
 }
 
 # 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)
+# give value of some identifier (response to showid; same values returned)
 idvalue = element idvalue               
-   {  name_attr, objtype_attr, pgmltext }
+   {  thyname_attr?, name_attr, objtype_attr, pgmltext }
 
 idtable    = element idtable { context_attr?, objtype_attr, identifier* }
 identifier = element identifier { token }
 
 context_attr = attribute context { token } # parent identifier (context) 
-
-instance_attr = attribute instance { text }
 
 # prover information: 
 # name, instance (e.g. in case of major parameter of invocation);
 # description, version, homepage,  welcome message, docs available
 proverinfo = element proverinfo 

      descr_attr?, url_attr?, filenameextns_attr?, 
 ## TEMP: these elements are duplicated in displayconfig, as they're
 ## moving there.  
       welcomemsg?, icon?, helpdoc*, lexicalstructure* }
 
-welcomemsg = element welcomemsg { text }
+instance_attr = attribute instance { token }
+
+welcomemsg = element welcomemsg { string }
 
 # 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"
-
-filenameextns_attr = attribute filenameextns { objnames }
+helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, token } # token string is arg to "viewdoc"
+
+filenameextns_attr = attribute filenameextns { xsd:NMTOKENS } # space-separated extensions sans "."
 
 # lexical structure of proof texts
 lexicalstructure = 
    element lexicalstructure {
       keyword*,

       commentdelimiter*,
       identifiersyntax?
    }
 
 keyword = element keyword {
-   attribute word { text },
+   attribute word { token },
    shorthelp?,
    longhelp? }
 
-shorthelp = element shorthelp { text }   # one-line (tooltip style) help 
-longhelp  = element longhelp { text }    # multi-line help
-
-stringdelimiter = element stringdelimiter { text }  # should be a single char
+shorthelp = element shorthelp { string }   # one-line (tooltip style) help 
+longhelp  = element longhelp { string }    # multi-line help
+
+stringdelimiter = element stringdelimiter { token }  # should be a single char
 
 # The escape character is used to escape strings and other special characters - in most languages it is \
-escapecharacter = element escapecharacter { text }  # should be a single char
+escapecharacter = element escapecharacter { token }  # should be a single char
 
 commentdelimiter = element commentdelimiter { 
-   attribute start { text },
-   attribute end { text }?,
+   attribute start { token },
+   attribute end { token }?,
    empty
   }
 
 
 # syntax for ids: id = initial allowed*  or id = allowed+ if initial empty
 identifiersyntax = element identifiersyntax { 
-   attribute initialchars { text }?,
-   attribute allowedchars { text }
+   attribute initialchars { token }?,
+   attribute allowedchars { token }
 }
 
 # ==============================================================================
 # 6. Prover Control
 # ==============================================================================

  | 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
+ | setproverflag		# set/clear a standard control flag (supersedes above)
 
 proverinit     = element proverinit { empty }  
 proverexit     = element proverexit { empty }
-startquiet     = element startquiet { empty }  
-stopquiet      = element stopquiet  { empty }  
-pgmlsymbolson  = element pgmlsymbolson { empty }
-pgmlsymbolsoff = element pgmlsymbolsoff { empty }
-
+startquiet     = element startquiet { empty }      # DEPRECATED 
+stopquiet      = element stopquiet  { empty }      # DEPRECATED 
+pgmlsymbolson  = element pgmlsymbolson { empty }   # DEPRECATED
+pgmlsymbolsoff = element pgmlsymbolsoff { empty }  # DEPRECATED
+
+setproverflag  = element setproverflag { flagname_attr, 
+					 attribute value { xsd:boolean } }
+flagname_attr  = 
+   attribute flagname { "quiet" 
+		      | "pgmlsymbols" 
+		      | "metainfo:thmdeps" 
+		      }
 
 # General prover output/responses
 
-# Nearly all prover output has an optional proverid attribute, except for the one which is 
-# never seen by any display. This is set by the Broker to indicate the originating or referring
-# prover. 
-# Displays rendering these messages can rely on this attribute being set.
+# Prover output has an otional proverid_attribute. This is set by the broker when relaying 
+# prover output to displays. When producing output, provers can and should not set this
+# attribute. 
 
 proveroutput =
    ready			# prover is ready for input
  | cleardisplay			# prover requests a display area to be cleared
  | proofstate			# prover outputs the proof state

  | parseresult			# results of a <parsescript> request (see later)
 
 ready = element ready { empty }
 
 displayarea = "status"		# a status line
-	    | "message"		# the message area (e.g. response buffer)
-            | "display"		# the main display area (e.g. goals buffer)
+	    | "message"		# the message area (e.g. response buffer, perhaps swapped into view)
+            | "display"		# the main display area (e.g. goals buffer, usually persistent)
 	    | token		# prover-specified window name
 
 cleardisplay = 
    element cleardisplay {
       proverid_attr?,

  | "information"		#  - user-level debug/info message (interface may hide)
  | "tracing"			#  - user-level "tracing" message (possibly voluminous)
 
 normalresponse =                           
   element normalresponse { 
-    proverid_attr?,
+    proverid_attr?,				    # if no proverid, assume message is from broker
     attribute area { displayarea },
     attribute messagecategory { messagecategory }?, # optional extra category (e.g. tracing/debug)
-    attribute urgent { "y" }?,                      # indication that message must be displayed
+    attribute urgent { xsd:boolean }?,              # message should be brought to users attention
     pgmltext 
 }
 
 ## Error messages:  these are different from ordinary messages in that
-##		    they indicate an error condition in the prover, with a notion
-##		    of fatality and (optionally) a location.  The interface may collect these
-##		    messages in a log, display in a modal dialog, or in the specified
-##		    display area if one is specified.
+## they indicate an error condition in the prover, with a notion
+## of fatality and (optionally) a location.  The interface may collect these
+## messages in a log, display in a modal dialog, or in the specified
+## display area if one is given
+## 
+## Error responses are also taken to indicate failure of a command to be processed, but only in
+## the special case of a response with fatality "fatal".  If any errorresponse with
+## fatality=fatal is sent before <ready/>, the PGIP command which triggered the message is
+## considered to have failed.  If the command is a scripting command, it will not be added to
+## the successfully processed part of the document.  A "nonfatal" error also indicates some
+## serious problem with the sent command, but it is not considered to have failed.  This is the
+## ordinary response for
 
 errorresponse = 
    element errorresponse { 
-     proverid_attr?,
+     proverid_attr?,				   #  ... as above ...
      attribute area { displayarea }?,
      attribute fatality { fatality },
      location_attrs,
      pgmltext
   }
 
 fatality =	  # degree of error conditions:
-   "nonfatal"     #  - warning message (interface should show message)
- | "fatal"        #  - error message (interface must show message)
+   "info"	  #  - info message
+ | "warning"      #  - warning message
+ | "nonfatal"     #  - error message, recovered and state updated
+ | "fatal"        #  - error message, command has failed
  | "panic"        #  - shutdown condition, component exits (interface may show message)
- | "log"          #  - log message (interface must not show message, write to broker log file)
- | "debug"        #  - debug message (interface may show message, write to broker log file)
-		   ## FIXME da: wondering if this is more appropriate than normal/internal above
-
+ | "log"          #  - system-level log message (interface does not show message; written to log file)
+ | "debug"        #  - system-level debug message (interface may show message; written to log file)
 
 # attributes describing a file location (for error messages, etc)
 location_attrs = 
-     attribute location_descr    { text }?,
+     attribute location_descr    { string }?,
      attribute location_url      { xsd:anyURI }?,
      attribute locationline      { xsd:positiveInteger }?,
      attribute locationcolumn    { xsd:positiveInteger }?,
-     attribute locationcharacter { xsd:positiveInteger }?
-
-scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, text }
+     attribute locationcharacter { xsd:positiveInteger }?,
+     attribute locationlength    { xsd:positiveInteger }?
+
+# instruction to insert some literal text into the document
+scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, string }
 
 
 # metainformation is an extensible place to put system-specific information
 
-value = element value { name_attr?, text }   # generic value holder
+value = element value { name_attr?, text }        # generic value holder [ deprecated: use metainfo ]
+metainfo = element metainfo { name_attr?, text }  # generic info holder
 
 metainforesponse = 
    element metainforesponse { 
       proverid_attr?,
-      attribute infotype { text },      # categorization of data
-      value* }                          # data values
+      attribute infotype { token },      # categorization of data
+      (value | metainfo)* }              # data values/text
 
 
 # ==============================================================================
 # 7. Proof script markup and proof control 
 # ==============================================================================
 
-# properproofcmds are purely markup on native proof script text
+# properproofcmds are purely markup on native proof script (plain) text
 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 proven, may close nested pf)
   | giveupgoal      # close current open proof, retaining attempt in script (Isar oops)
   | postponegoal    # close current open proof, record as proof obl'n  (Isar sorry)  
   | comment         # a proof script comment; text probably ignored by prover 
+  | doccomment      # a proof script document comment; text maybe processed by prover 
   | whitespace      # a whitespace comment; text ignored by prover
   | spuriouscmd     # command ignored for undo, e.g. "print x", could be pruned from script
   | badcmd          # a command which should not be stored in the script (e.g. an improperproofcmd)
-  | litcomment      # a literate comment (never passed to prover)
+  | litcomment      # a PGIP literate comment (never passed to prover)
   | pragma	    # a document generating instruction (never passed to prover)
 
 # improperproofcmds are commands which are never stored in the script
 improperproofcmd =
     dostep        # issue a properproofcmd (without passing in markup)

   | redostep      # redo the last undone step issued in currently open goal (optionally supported)
   | 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
 
-opengoal     = element opengoal     { display_attr?, thmname_attr?, text } # FIXME: add objprefval
-proofstep    = element proofstep    { display_attr?, name_attr?, objtype_attr?, text }
-closegoal    = element closegoal    { display_attr?, text }
-giveupgoal   = element giveupgoal   { display_attr?, text }
-postponegoal = element postponegoal { display_attr?, text }
-comment      = element comment      { display_attr?, text }
-whitespace   = element whitespace   { display_attr?, text }
+# In future we may allow input to contain markup; for now it is treated uniformly as plain text.
+
+opengoal     = element opengoal     { display_attr?, thmname_attr?, string } # FIXME: add objprefval
+proofstep    = element proofstep    { display_attr?, name_attr?, objtype_attr?, string }
+closegoal    = element closegoal    { display_attr?, string }
+giveupgoal   = element giveupgoal   { display_attr?, string }
+postponegoal = element postponegoal { display_attr?, string }
+comment      = element comment      { display_attr?, string }
+doccomment   = element doccomment   { display_attr?, string }
+whitespace   = element whitespace   { display_attr?, string }
 
 display_attr = attribute nodisplay { xsd:boolean }  # whether to display in documentation
 
-spuriouscmd  = element spuriouscmd { text }
-badcmd       = element badcmd { text }
+spuriouscmd  = element spuriouscmd { string }  # no semantic effect (e.g. print)
+badcmd       = element badcmd { string }       # illegal in script (e.g. undo)
+nonscripting = element nonscripting { string } # non-scripting text (different doc type)
 
 litcomment  = element litcomment { format_attr?, (text | directive)* }
 directive   = element directive { (proofctxt,pgml) }
 format_attr = attribute format { token }
 
 pragma       = showhidecode | setformat
 showhidecode = element showcode { attribute show { xsd:boolean } }
 setformat    = element setformat { format_attr }
 
-dostep       = element dostep { text }
-undostep     = element undostep { empty }
-redostep     = element redostep { empty }
+dostep       = element dostep { string }
+undostep     = element undostep { times_attr? }
+redostep     = element redostep { times_attr? }
 abortgoal    = element abortgoal { empty }
 forget       = element forget { thyname_attr?, name_attr?, objtype_attr? }
 restoregoal  = element restoregoal { thmname_attr }
 
+times_attr   = attribute times { xsd:positiveInteger }
+
 # empty objprefval element is used for object prefs in script markup 
 objprefval = element objprefval { name_attr, val_attr, empty }
-val_attr   = attribute value { text }
+val_attr   = attribute value { token }
 
 
 
 
 # =======================================================
 # Inspecting the proof context, etc.
 
+# NB: ids/refs/parent: work in progress, liable to change.
+
 proofctxt =
-    askids         # please tell me about identifiers (given objtype in a theory)
-  | showid         # print value of an object
-  | askguise       # please tell me about the current state of the prover
+    askids         # tell me about identifiers (given objtype in a theory)
+  | askrefs        # tell me about dependencies (references) of an identifier
+#  | askparent      # tell me the container for some identifier
+  | showid         # print the value of some object
+  | askguise       # tell me about the current state of the prover
   | parsescript    # parse a raw proof script into proofcmds
   | 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

 askids = element askids  { thyname_attr?, objtype_attr? }
 	# Note that thyname_attr is *required* for certain objtypes (e.g. theorem).
 	# This is because otherwise the list is enormous.
 	# Perhaps we should make thyname_attr obligatory? 
 	# With a blank entry (i.e. thyname="") allowed for listing theories, or for when 
-	# you really do want to see everything.
+	# you really do want to see everything (could be a shell-style glob)
+
+
+# askids:    container -> identifiers contained within
+# askparent: identifier + type + context -> container
+# askrers:   identifier + type + context -> identifiers which are referenced 
+#
+askrefs = element askrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr? }
+# TODO: maybe include guises here as indication of reference point.  
+# setrefs in reply to askrefs only really needs identifiers, but it's nice to
+# support voluntary information too.
+setrefs = element setrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr?, idtable*, fileurl* }
+fileurl = element fileurl { url_attr }
+# telldeps = element telldeps { thyname_attr?, objtype_attr, name_attr?, identifier* }
+# Idea: for a theory dependency we return a single file (URL), the containing file.
+#       for a file dependency we return urls of parent files,
+#       for theorem dependency we return theory
+#       for term dependency we return definition (point in file)
+
 
 showid = element showid  { thyname_attr?, objtype_attr, name_attr }
 
 askguise = element askguise { empty }
 
+showproofstate = element showproofstate { empty }
+showctxt       = element showctxt { empty }
+searchtheorems = element searchtheorems { string }
+setlinewidth   = element setlinewidth { xsd:positiveInteger }
+viewdoc        = element viewdoc { token }
+
 
 # =======================================================
-# Parsing proof scripts
+# Proof script documents and parsing proof scripts
+
+# A PGIP document is a sequence of script commands, each of which
+# may have meta information attached.
+properscriptcmdmetainfo = properscriptcmd, metainfo*
+pgipdoc = element pgipdoc { properscriptcmdmetainfo* }
+
 
 # NB: parsing needs only be supported for "proper" proof commands,
 # which may appear in proof texts.  The groupdelimiters are purely
 # markup hints to the interface for display structure on concrete syntax.
 # The location attributes can be used by the prover in <parsescript> to

 # particularly in the case of (re-)parsing only part of a file.
 # The parsing component MUST return the same location attributes
 # (and system data attribute) that was passed in.
 
 parsescript = element parsescript
-                 { location_attrs, systemdata_attr, text }
+                 { location_attrs, systemdata_attr, string }
        
 parseresult = element parseresult { location_attrs, systemdata_attr,
 				    singleparseresult* }
 
-singleparseresult  = properscriptcmd | unparseable | errorresponse
-
-unparseable = element unparseable { text }
+# Really we'd like parsing to return properscriptcmdmetainfo as a single
+# result (and similarly for newobj).  
+# Unfortunately, although this is an XML-transparent extension, it
+# messes up the Haskell schema-fixed code rather extensively, so for
+# now we just treat metainfo at the same level as the other results,
+# although it should only appear following a properscriptcmd.
+
+singleparseresult  = properscriptcmd | metainfo | unparseable | errorresponse
+
+unparseable = element unparseable { string }
 properscriptcmd = properproofcmd | properfilecmd | groupdelimiter
 
 
+
+
 groupdelimiter = openblock | closeblock
-openblock  = element openblock { metavarid_attr? }
+openblock  = element openblock { 
+   name_attr?, objtype_attr?, 
+   metavarid_attr?, positionid_attr?,
+   fold_attr?, indent_attr? }
 closeblock = element closeblock { empty }
 
 # 
-metavarid_attr = attribute metavarid { token }
-
-showproofstate = element showproofstate { empty }
-showctxt       = element showctxt { empty }
-searchtheorems = element searchtheorems { text }
-setlinewidth   = element setlinewidth { xsd:positiveInteger }
-viewdoc        = element viewdoc { text }
+metavarid_attr  = attribute metavarid { token }
+positionid_attr = attribute positionid { token }
+fold_attr       = attribute fold { xsd:boolean }
+indent_attr     = attribute indent { xsd:integer }
 
 
 # =======================================================
 # Theory/file handling
 

     doitem	    # issue a proper file command (without passing in markup)
   | undoitem	    # undo last step (or named item) in theory construction
   | redoitem	    # redo last step (or named item) in theory construction (optionally supported)
   | 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
+  | openfile        # signal a file is being opened for constructing a proof text interactively
+  | closefile       # close the currently open 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)
+  | loadfile        # load (i.e. process directly) a file possibly containing theory definition(s)
+  | retractfile     # retract a given file (including all contained theories) 
   | changecwd       # change prover's working directory (or load path) for files
   | systemcmd       # system (other) command, parsed internally
 
 fileinfomsg = 
    informfileloaded       # prover informs interface a particular file is loaded
  | informfileretracted    # prover informs interface a particular file is outdated
  | informguise		  # prover informs interface about current state
 
-opentheory    = element opentheory    { thyname_attr, parentnames_attr?, text }
-closetheory   = element closetheory   { text }
-theoryitem    = element theoryitem    { name_attr?, objtype_attr?, text } # FIXME: add objprefval
-
-doitem        = element doitem        { text } 
-undoitem      = element undoitem      { name_attr?, objtype_attr? } 
-redoitem      = element redoitem      { name_attr?, objtype_attr? } 
+opentheory    = element opentheory    { thyname_attr, parentnames_attr?, string }
+closetheory   = element closetheory   { string }
+theoryitem    = element theoryitem    { name_attr?, objtype_attr?, string } # FIXME: add objprefval
+
+doitem        = element doitem        { string } 
+undoitem      = element undoitem      { name_attr?, objtype_attr?, times_attr? } 
+redoitem      = element redoitem      { name_attr?, objtype_attr?, times_attr? } 
 aborttheory   = element aborttheory   { empty }
 retracttheory = element retracttheory { thyname_attr }
 
 parentnames_attr = attribute parentnames { objnames }
 

 
 openfile      = element openfile  { url_attr }	    # notify begin reading from given file
 closefile     = element closefile { empty }	    # notify currently open file is complete
 abortfile     = element abortfile { empty }	    # notify currently open file is discarded
 loadfile      = element loadfile  { url_attr }	    # ask prover to read file directly
-changecwd     = element changecwd { dir_attr }	    # ask prover to change current working dir
+retractfile   = element retractfile { url_attr }    # ask prover to retract file
+changecwd     = element changecwd { url_attr }	    # ask prover to change current working dir
 
 # this one not yet implemented, but would be handy.  Perhaps could be 
 # locatethy/locatefile instead.
 #locateobj     = element locateobj { name_attr, objtype_attr } # ask prover for file defining obj
 
-informfileloaded    = element informfileloaded    { url_attr }  # prover indicates a processed file
-informfileretracted = element informfileretracted { url_attr }  # prover indicates an undone file
+informfileloaded    = element informfileloaded    { completed_attr?, 
+						    url_attr }  # prover indicates a processed file
+informfileretracted = element informfileretracted { completed_attr?, 
+						    url_attr }  # prover indicates an undone file
+informfileoutdated = element informfileoutdated { completed_attr?, 
+						    url_attr }  # prover indicates an outdated file
+
 informfilelocation  = element informfilelocation  { url_attr }  # response to locateobj
+
+completed_attr = attribute completed { xsd:boolean }  # false if not completed (absent=>true)
+						      # (the prover is requesting a lock)
+
+
 
 informguise = 
    element informguise {
       element guisefile { url_attr }?,
       element guisetheory { thyname_attr }?,
       element guiseproof { thmname_attr?, proofpos_attr? }?
    }
 
 proofpos_attr = attribute proofpos { xsd:nonNegativeInteger }
 
-systemcmd     = element systemcmd     { text }		# "shell escape", arbitrary prover command!
-
-# ==============================================================================
-# 8. Internal messages-- only used between communicating brokers.
+systemcmd     = element systemcmd     { string }	# "shell escape", arbitrary prover command!
+
+# ==============================================================================
+# 8. Internal messages: only used between communicating brokers.
 # ==============================================================================
 internalmsg  = launchcomp | stopcomp | registercomp | compstatus
 
 launchcomp   = element launchcomponent { componentspec }
 	               # request to start an instance of this component remotely
-stopcomp     = element stopcomponent { attribute sessionid { string } }
+stopcomp     = element stopcomponent { attribute sessionid { token } }
                        # request to stop component with this session id remotely
 
 registercomp = element registercomponent { activecompspec } 
                        # component has been started successfully
 compstatus   = element componentstatus { componentstatus_attr    # status
 	                               , componentid_attr?       # component id (for failure)
-	                               , element text { text }?  # user-visible error message
-				       , element info { text }?  # Additional info for log files.
+	                               , element text { string }?  # user-visible error message
+				       , element info { string }?  # Additional info for log files.
 				       }	
                        # component status: failed to start, or exited
 
 componentstatus_attr = attribute status { ("fail"   # component failed to start
  		                          |"exit"  # component exited