Proof General PGIP/PGML Schema
namespace local = ""
namespace inh = inherit
namespace a = "http://relaxng.org/ns/compatibility/annotations/1.0"

include "pgml.rnc"

name_attr = attribute name { token }

thyname_attr = attribute thyname { token }

thmname_attr = attribute thmname { token }

datetime_attr = attribute datetime { xsd:dateTime }

url_attr = attribute url { xsd:anyURI }

dir_attr = attribute dir { string }

systemdata_attr = attribute systemdata { token }?

objname = token

objnames = token

start = pgippgipsdisplayconfigpgipconfigpgipdoc

pgip = element pgip { pgip_attrs, ( toprovermsgtodisplaymsgfromprovermsgfromdisplaymsginternalmsg ) }

pgips = element pgips { pgip+ }

pgip_attrs =
attribute tag { token }?,
attribute id { token },
attribute destid { token }?,
attribute class { pgip_class },
attribute refid { token }?,
attribute refseq { xsd:positiveInteger }?,
attribute seq { xsd:positiveInteger }

pgip_class = "pg""pa""pd"

toprovermsg =
proverconfigprovercontrolimproperproofcmdimproperfilecmdproperproofcmdproperfilecmdproofctxt

fromprovermsg = kitconfigproveroutputfileinfomsg

todisplaymsg = brokermsgdispmsg

fromdisplaymsg = dispcmdbrokercontrol

pgipconfig = element pgipconfig { componentspec* }

componentspec =
element componentspec
{
componentid_attr, componentname_attr, componenttype, startupattrs, systemattrs, componentconnect
}

componentid_attr = attribute componentid { token }

componentname_attr = attribute componentname { token }

componenttype = element componenttype { provercomponentdisplaycomponentparsercomponentothercomponent }

provercomponent = element provercomponent { empty }

displaycomponent = element displaycomponent { attribute active { xsd:boolean }? }

parsercomponent = element parsercomponent { componentid_attr }

othercomponent = element othercomponent { empty }

componentconnect = componentsubprocesscomponentsocketconnectbyproxy

componentsubprocess = element syscommand { string }

componentsocket = element host { token }, element port { xsd:positiveInteger }

connectbyproxy =
element proxy
{
attribute host { token },
attribute connect { "rsh""ssh""server" }?,
attribute user { token }?,
attribute path { token }?,
attribute port { xsd:positiveInteger }?,
componentconnect
}

startupattrs = attribute startup { "boot""manual""ignore" }?

systemattrs =
attribute timeout { xsd:integer }?, attribute sync { xsd:boolean }?, attribute nestedgoals { xsd:boolean }?

brokercontrol =
launchproverexitproverrestartproverproversqueryshutdownbrokerbrokerstatusquerypgipconfig

provername_attr = attribute provername { provername }

provername = token

proverid_attr = attribute proverid { proverid }

proverid = token

launchprover = element launchprover { componentid_attr }

exitprover = element exitprover { proverid_attr }

restartprover = element restartprover { proverid_attr }

proversquery = element proversavailable { empty }

brokerstatusquery = element brokerstatusquery { empty }

shutdownbroker = element shutdownbroker { attribute force { xsd:boolean }? }

brokermsg = brokerstatusproveravailmsgnewprovermsgproverstatemsg

brokerstatus = element brokerstatus { knownprovers, runningprovers, brokerinformation }

knownprover = element knownprover { componentid_attr, provername }

runningprover = element runningprover { componentid_attr, proverid_attr, provername }

knownprovers = element knownprovers { knownprover* }

runningprovers = element runningprovers { runningprover* }

brokerinformation = element brokerinformation { string }

proveravailmsg = element proveravailable { provername_attr, componentid_attr }

newprovermsg = element proverstarted { proverid_attr, componentid_attr, provername_attr }

proverstatemsg = element proverstate { proverid_attr, provername_attr, attribute proverstate { proverstate } }

proverstate = "ready""busy""exitus"

dispcmd = dispfilecmddispobjcmd

dispmsg = dispfilemsgdispobjmsg

dispfilecmd = loadparsefilenewfilewithdispopenfilesavefilediscardfile

dispfilemsg = newfilefilestatus

srcid_attr = attribute srcid { token }

loadparsefile = element loadparsefile { url_attr, proverid_attr }

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, url_attr?, datetime_attr }

newstatus_attr = attribute newstatus { "saved""changed""discarded" }

dispobjcmd = setobjstateeditobjcreateobjinputcmdinterruptprover

dispobjmsg = element dispobjmsg { newobj+ | delobj+ | replaceobjsobjectstate+ }

newobj =
element newobj
{
proverid_attr,
srcid_attr,
objid_attr,
attribute objposition { objid }?,
objtype_attr?,
attribute objparent { objid }?,
attribute objstate { objstate },
( properscriptcmdunparseable )
}

replaceobjs =
element replaceobjs
{
srcid_attr,
attribute replacedfrom { objid }?,
attribute replacedto { objid }?,
delobj*,
newobj*
}

delobj = element delobj { proverid_attr, srcid_attr, objid_attr }

## update to display

objectstate = element objstate { proverid_attr, srcid_attr, objid_attr, attribute newstate { objstate } }

## update from display

setobjstate = element setobjstate { objid_attr, attribute newstate { objstate } }

editobj = element editobj { srcid_attr?, attribute editfrom { objid }?, attribute editto { objid }?, string }

createobj = element createobj { srcid_attr?, attribute objposition { objid }?, string }

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 = token

objstate = "unparseable""parsed""being_processed""processed""outdated"

proverconfig = askpgipaskpgmlaskconfigaskprefssetprefgetpref

prefcat_attr = attribute prefcategory { token }

askpgip = element askpgip { empty }

askpgml = element askpgml { empty }

askconfig = element askconfig { empty }

askprefs = element askprefs { prefcat_attr? }

setpref = element setpref { name_attr, prefcat_attr?, pgipvalue }

getpref = element getpref { name_attr, prefcat_attr? }

kitconfig =
usespgip
usespgml
pgmlconfig
proverinfo
hasprefs
prefval
displayconfig
setids
addids
delids
idvalue
menuadd
menudel

version_attr = attribute version { token }

usespgml = element usespgml { version_attr }

usespgip = element usespgip { version_attr, activecompspec }

activecompspec = componentid_attr?, componentname_attr?, componenttype?, systemattrs, acceptedpgipelems?

acceptedpgipelems = element acceptedpgipelems { singlepgipelem* }

singlepgipelem = element pgipelem { attribute async { xsd:boolean }?, attribute attributes { text }?, text }

pgmlconfig = element pgmlconfig { pgmlconfiguration }

pgiptype = pgipnullpgipboolpgipintpgipstringpgipchoicepgipconst

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 { descr_attr?, empty }

pgipconst = element pgipconst { name_attr, descr_attr?, empty }

pgipchoice = element pgipchoice { pgiptype+ }

pgipvalue = string

icon = element icon { xsd:base64Binary }

default_attr = attribute default { token }

descr_attr = attribute descr { string }

haspref = element haspref { name_attr, descr_attr?, default_attr?, icon?, pgiptype }

hasprefs = element hasprefs { prefcat_attr?, haspref* }

prefval = element prefval { name_attr, pgipvalue }

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 }

displayconfig = element displayconfig { welcomemsg?, icon?, helpdoc*, lexicalstructure*, objtype*, opn* }

objtype = element objtype { name_attr, descr_attr?, icon?, contains*, hasprefs? }

objtype_attr = attribute objtype { token }

contains = element contains { objtype_attr, empty }

opn = element opn { name_attr, descr_attr?, inputform?, opsrc*, optrg, opcmd, improper_attr? }

opsrc = element opsrc { name_attr?, selnumber_attr?, prompt_attr?, listwithsep_attr?, list { token* } }

listwithsep_attr = attribute listwithsep { token }

selnumber_attr = attribute selnumber { xsd:positiveInteger }

prompt_attr = attribute prompt { string }

optrg = element optrg { token }?

opcmd = element opcmd { string }

inputform = element inputform { field+ }

field = element field { name_attr, pgiptype, element prompt { string } }

setids = element setids { idtable* }

addids = element addids { idtable* }

delids = element delids { idtable* }

idvalue = element idvalue { thyname_attr?, name_attr, objtype_attr, pgml }

idtable = element idtable { context_attr?, objtype_attr, identifier* }

identifier = element identifier { token }

context_attr = attribute context { token }

proverinfo =
element proverinfo
{
name_attr,
version_attr?,
instance_attr?,
descr_attr?,
url_attr?,
filenameextns_attr?,
## TEMP: these elements are duplicated in displayconfig, as they're
## moving there.

welcomemsg?,
icon?,
helpdoc*,
lexicalstructure*
}

instance_attr = attribute instance { token }

welcomemsg = element welcomemsg { string }

helpdoc = element helpdoc { name_attr, descr_attr, url_attr?, token }

filenameextns_attr = attribute filenameextns { xsd:NMTOKENS }

lexicalstructure =
element lexicalstructure { keyword*, stringdelimiter?, escapecharacter?, commentdelimiter*, identifiersyntax? }

keyword = element keyword { attribute word { token }, shorthelp?, longhelp? }

shorthelp = element shorthelp { string }

longhelp = element longhelp { string }

stringdelimiter = element stringdelimiter { token }

escapecharacter = element escapecharacter { token }

commentdelimiter = element commentdelimiter { attribute start { token }, attribute end { token }?, empty }

identifiersyntax = element identifiersyntax { attribute initialchars { token }?, attribute allowedchars { token } }

provercontrol = proverinitproverexitsetproverflag

proverinit = element proverinit { empty }

proverexit = element proverexit { empty }

setproverflag = element setproverflag { flagname_attr, attribute value { xsd:boolean } }

flagname_attr = attribute flagname { "quiet""pgmlsymbols""metainfo:thmdeps" }

proveroutput = readynormalresponseerrorresponsescriptinsertmetainforesponseparseresult

ready = element ready { empty }

normalresponse = element normalresponse { proverid_attr?, pgml }

## 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 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
## 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?, attribute fatality { fatality }, location_attrs, pgml }

fatality = "info""warning""nonfatal""fatal""panic""log""debug"

location_attrs =
attribute location_descr { string }?,
attribute location_url { xsd:anyURI }?,
attribute locationline { xsd:positiveInteger }?,
attribute locationcolumn { xsd:positiveInteger }?,
attribute locationcharacter { xsd:positiveInteger }?,
attribute locationlength { xsd:positiveInteger }?

scriptinsert = element scriptinsert { proverid_attr?, metavarid_attr?, string }

value = element value { name_attr?, text }

metainfo = element metainfo { name_attr?, text }

metainforesponse = element metainforesponse { proverid_attr?, attribute infotype { token }, ( valuemetainfo )* }

properproofcmd =
opengoal
proofstep
closegoal
giveupgoal
postponegoal
comment
doccomment
whitespace
spuriouscmd
badcmd
litcomment
pragma

improperproofcmd = dostepundostepredostepabortgoalforgetrestoregoal

scriptmarkup = pgmltext

opengoal = element opengoal { thmname_attr?, scriptmarkup }

proofstep = element proofstep { name_attr?, objtype_attr?, scriptmarkup }

closegoal = element closegoal { scriptmarkup }

giveupgoal = element giveupgoal { scriptmarkup }

postponegoal = element postponegoal { scriptmarkup }

comment = element comment { scriptmarkup }

doccomment = element doccomment { scriptmarkup }

whitespace = element whitespace { scriptmarkup }

spuriouscmd = element spuriouscmd { scriptmarkup }

badcmd = element badcmd { scriptmarkup }

nonscripting = element nonscripting { scriptmarkup }

litcomment = element litcomment { format_attr?, ( textdirective )* }

directive = element directive { proofctxt, pgml }

format_attr = attribute format { token }

pragma = showhidecodesetformat

showhidecode = element showcode { attribute show { xsd:boolean } }

setformat = element setformat { format_attr }

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 }

objprefval = element objprefval { name_attr, val_attr, empty }

val_attr = attribute value { token }

proofctxt =
askids
askrefs
showid
askguise
parsescript
showproofstate
showctxt
searchtheorems
setlinewidth
viewdoc

askids = element askids { thyname_attr?, objtype_attr? }

askrefs = element askrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr? }

setrefs = element setrefs { url_attr?, thyname_attr?, objtype_attr?, name_attr?, idtable*, fileurl* }

fileurl = element fileurl { url_attr }

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 }

properscriptcmdmetainfo = properscriptcmd, metainfo*

pgipdoc = element pgipdoc { properscriptcmdmetainfo* }

parsescript = element parsescript { location_attrs, systemdata_attr, string }

parseresult = element parseresult { location_attrs, systemdata_attr, singleparseresult* }

singleparseresult = properscriptcmdmetainfounparseableerrorresponse

unparseable = element unparseable { scriptmarkup }

properscriptcmd = properproofcmdproperfilecmdgroupdelimiter

groupdelimiter = openblockcloseblock

openblock =
element openblock
{
name_attr?,
objtype_attr?,
metavarid_attr?,
positionid_attr?,
fold_attr?,
indent_attr?,
display_attr?
}

closeblock = element closeblock { empty }

metavarid_attr = attribute metavarid { token }

positionid_attr = attribute positionid { token }

fold_attr = attribute fold { xsd:boolean }

indent_attr = attribute indent { xsd:integer }

display_attr = attribute nodisplay { xsd:boolean }

properfilecmd = opentheorytheoryitemclosetheory

improperfilecmd =
doitem
undoitem
redoitem
aborttheory
retracttheory
openfile
closefile
abortfile
loadfile
retractfile
changecwd
systemcmd

fileinfomsg = informfileloadedinformfileretractedinformguise

opentheory = element opentheory { thyname_attr, parentnames_attr?, scriptmarkup }

closetheory = element closetheory { scriptmarkup }

theoryitem = element theoryitem { name_attr?, objtype_attr?, scriptmarkup }

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 }

closefile = element closefile { empty }

abortfile = element abortfile { empty }

loadfile = element loadfile { url_attr }

retractfile = element retractfile { url_attr }

changecwd = element changecwd { url_attr }

informfileloaded = element informfileloaded { completed_attr?, url_attr }

informfileretracted = element informfileretracted { completed_attr?, url_attr }

informfileoutdated = element informfileoutdated { completed_attr?, url_attr }

informfilelocation = element informfilelocation { url_attr }

completed_attr = attribute completed { xsd:boolean }

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 { string }

internalmsg = launchcompstopcompregistercompcompstatus

launchcomp = element launchcomponent { componentspec }

stopcomp = element stopcomponent { attribute sessionid { token } }

registercomp = element registercomponent { activecompspec }

compstatus =
element componentstatus
{
componentstatus_attr, componentid_attr?, element text { string }?, element info { string }?
}

componentstatus_attr = attribute status { "fail""exit" }
pgml.rnc
 
namespace local = ""
namespace inh = inherit
namespace a = "http://relaxng.org/ns/compatibility/annotations/1.0"

## PGML terms with pretty printing, actions, references and embedded objects.
## PGML terms with pretty printing, actions, references and embedded objects.

term = symatomboxbreaksubtermaltembedtext

## A named symbol may have a previously configured alternative
## rendering (see below) or be rendered as the given text

sym = element sym { symname_attr, text }

symname_attr = attribute name { xsd:NMTOKEN }

## An atom is some text (maybe including symbols), with an optional
## kind which may control its printing by a prover-specific style
## sheet.

atom = element atom { kind_attr?, ( textsym )* }

kind_attr = attribute kind { token }

## A box whose children may be displayed with different layout strategies, using
## the directives of BoxML (see http://helm.cs.unibo.it/mml-widget/qna.html).
## The children of the box may have: fixed horizontal or vertical layout,
## horizontal or vertical with inconsistent breaking ("hov", the default),
## or horizontal or vertical with consistent breaking ("hv").
## Inside a box, the given indentation space is applied to children
## if a line break is added. Note and spaces/newlines in the markup are
## NOT obeyed (explicit spaces must be given with atoms).

box = element box { orient_attr?, indent_att?, term* }

orient_attr = attribute orient { "hov""h""v""hv" }

indent_att = attribute indent { xsd:integer }

## A line/column breaking hint. The indentation is added if the line
## is not broken. Consistent breaking will take all breaks at the same level.

break = element break { mandatory_attr?, indent_att? }

mandatory_attr = attribute mandatory { xsd:boolean }

## An annotated subterm. This may be used to:
## - subdivide large displays (e.g. goal state by subgoals, assumptions) using the kind and parameter tokens (system specific interpretation); - mark an identifer or term with an objtype (and perhaps a global name); - decorate a region with a bold, italic, or other highlight (e.g., to markup error/warning/info areas with squiggles red/yellow/blue). - reference to a content model with position annotations - indicate an action such as a system-specific menu, folding ("toggle") or render a button - give a cross reference to the defining point of some text (e.g. file URL with line.column fragment)
## - subdivide large displays (e.g. goal state by subgoals, assumptions)
## using the kind and parameter tokens (system specific interpretation);
## - mark an identifer or term with an objtype (and perhaps a global name);
## - decorate a region with a bold, italic, or other highlight (e.g.,
## to markup error/warning/info areas with squiggles red/yellow/blue).
## - reference to a content model with position annotations
## - indicate an action such as a system-specific menu, folding ("toggle")
## or render a button
## - give a cross reference to the defining point of some text
## (e.g. file URL with line.column fragment)

subterm =
element subterm
{
skind_attr?,
sparam_attr?,
splace_attr?,
sdec_attr?,
sobjtype_attr?,
sname_attr?,
saction_attr?,
spos_attr?,
sref_attr?,
term
}

skind_attr = attribute kind { token }

sparam_attr = attribute param { token }

splace_attr = attribute place { "sub""super""above""below" }

sobjtype_attr = attribute objtype { token }

sname_attr = attribute name { token }

sdec_attr = attribute decoration { "bold""italic""error""warning""information"token }

saction_attr = attribute action { "toggle""button""menu" }

spos_attr = attribute pos { token }

sref_attr = attribute xref { xsd:anyURI }

## Alternative subtrees. This may be used to select between subtrees based on
## the kind, for example, alternate renderings according available space, or
## alternate embedded objects according to target language.

alt = element alt { altkind_attr, term* }

altkind_attr = attribute kind { token }

## An embedded object. The object embedded would typically be in a
## different markup language (e.g. MathML).

embed = element embed { text }

## PGML documents
## PGML documents

pgml = element pgml { pgml_version_attr?, systemid_attr?, area_attr?, term* }

## Version of PGML. Useful for standalone documents. Broker may add.

pgml_version_attr = attribute version { xsd:NMTOKEN }

## System that produced PGML. Useful for standalone documents. Broker may add.

systemid_attr = attribute systemid { token }

## Display area (e.g., window) for showing message. Only relevant for output;
## default area is message in this case.

area_attr = attribute area { "status""message""display""tracing""internal"token }

## This schema is embedded into the PGIP schema. If we would
## keep them separate, we would add the start production here:

## Symbol configuration The sym element can be rendered in three different ways, in descending preference order: 1) one of the previously configured alternatives for the symbol, available in a prover-specific configuration, see below. 2) the PGML symbol given by the name attribute, if one of standard (TeX-ish) names given elsewhere (deprecated). 3) the text content of the SYM element, if non-empty The symbol configuration allows flexible choice between different renderings.
## Symbol configuration
## The sym element can be rendered in three different ways, in descending preference order: 1) one of the previously configured alternatives for the symbol, available in a prover-specific configuration, see below. 2) the PGML symbol given by the name attribute, if one of standard (TeX-ish) names given elsewhere (deprecated). 3) the text content of the SYM element, if non-empty The symbol configuration allows flexible choice between different renderings.
## The sym element can be rendered in three different ways,
## in descending preference order:
## 1) one of the previously configured alternatives for the symbol, available in a prover-specific configuration, see below. 2) the PGML symbol given by the name attribute, if one of standard (TeX-ish) names given elsewhere (deprecated). 3) the text content of the SYM element, if non-empty The symbol configuration allows flexible choice between different renderings.
## 1) one of the previously configured alternatives for the symbol,
## available in a prover-specific configuration, see below.
## 2) the PGML symbol given by the name attribute, if one of
## standard (TeX-ish) names given elsewhere (deprecated).
## 3) the text content of the SYM element, if non-empty
## The symbol configuration allows flexible choice between different renderings.
## The symbol configuration allows flexible choice between
## different renderings.

## A configuration of PGML is a sequence of symbol configurations

pgmlconfiguration = symconfig*

## A symbol configuration provides: a (unique) symbol name, used in the <sym> element a family name (user documentation only) a unicode character sequence an HTML alternative using HTML entities (in plain ASCII) a plain text alternative for impoverished ASCII displays a token text which can be used in the document in place of the unicode sequence to store files in a poorer ASCII/latin/other encoding a typing shortcut that may be supported by editors in displays an xml rendering (in some other XML schema) e.g. <symconfig name="Forall" family="Symbols" unicode="∀" shortcut="all " html="&forall;" token="\<forall>" alt="ALL" /> Symbol configurations are prover specific. They may be shared between displays, although different displays may use different parts of configurations.
## A symbol configuration provides:
## a (unique) symbol name, used in the <sym> element a family name (user documentation only) a unicode character sequence an HTML alternative using HTML entities (in plain ASCII) a plain text alternative for impoverished ASCII displays a token text which can be used in the document in place of the unicode sequence to store files in a poorer ASCII/latin/other encoding a typing shortcut that may be supported by editors in displays an xml rendering (in some other XML schema) e.g. <symconfig name="Forall" family="Symbols" unicode="∀" shortcut="all " html="&forall;" token="\<forall>" alt="ALL" /> Symbol configurations are prover specific. They may be shared between displays, although different displays may use different parts of configurations.
## a (unique) symbol name, used in the <sym> element
## a family name (user documentation only)
## a unicode character sequence
## an HTML alternative using HTML entities (in plain ASCII)
## a plain text alternative for impoverished ASCII displays
## a token text which can be used in the document in place of the unicode sequence
## to store files in a poorer ASCII/latin/other encoding
## a typing shortcut that may be supported by editors in displays
## an xml rendering (in some other XML schema)
##
## e.g.
## <symconfig name="Forall" family="Symbols" unicode="∀" shortcut="all " html="&forall;" token="\<forall>" alt="ALL" /> Symbol configurations are prover specific. They may be shared between displays, although different displays may use different parts of configurations.
## <symconfig name="Forall" family="Symbols" unicode="∀" shortcut="all "
## html="&forall;" token="\<forall>" alt="ALL" />
## Symbol configurations are prover specific. They may be shared between displays, although different displays may use different parts of configurations.
## Symbol configurations are prover specific. They may be shared
## between displays, although different displays may use different
## parts of configurations.

symconfig =
element symconfig
{
symname_attr,
family_attr?,
unicode_attr?,
html_attr?,
textalt_attr?,
token_attr?,
shortcut_attr?,
xmlrender?
}

family_attr = attribute family { string }

unicode_attr = attribute unicode { string }

html_attr = attribute html { string }

textalt_attr = attribute alt { string }

token_attr = attribute token { string }

shortcut_attr = attribute shortcut { string }

xmlrender = element xmlrender { text }
Index
 
start
Definitions: 1
abortfile
Definitions: 1
Referenced from:
improperfilecmd
abortgoal
Definitions: 1
Referenced from:
improperproofcmd
aborttheory
Definitions: 1
Referenced from:
improperfilecmd
acceptedpgipelems
Definitions: 1
Referenced from:
activecompspec
activecompspec
Definitions: 1
Referenced from:
registercomp
usespgip
addids
Definitions: 1
Referenced from:
kitconfig
alt
Definitions: 1
Referenced from:
term
altkind_attr
Definitions: 1
Referenced from:
alt
area_attr
Definitions: 1
Referenced from:
pgml
askconfig
Definitions: 1
Referenced from:
proverconfig
askguise
Definitions: 1
Referenced from:
proofctxt
askids
Definitions: 1
Referenced from:
proofctxt
askpgip
Definitions: 1
Referenced from:
proverconfig
askpgml
Definitions: 1
Referenced from:
proverconfig
askprefs
Definitions: 1
Referenced from:
proverconfig
askrefs
Definitions: 1
Referenced from:
proofctxt
atom
Definitions: 1
Referenced from:
term
badcmd
Definitions: 1
Referenced from:
properproofcmd
box
Definitions: 1
Referenced from:
term
break
Definitions: 1
Referenced from:
term
brokercontrol
Definitions: 1
Referenced from:
fromdisplaymsg
brokerinformation
Definitions: 1
Referenced from:
brokerstatus
brokermsg
Definitions: 1
Referenced from:
todisplaymsg
brokerstatus
Definitions: 1
Referenced from:
brokermsg
brokerstatusquery
Definitions: 1
Referenced from:
brokercontrol
changecwd
Definitions: 1
Referenced from:
improperfilecmd
closeblock
Definitions: 1
Referenced from:
groupdelimiter
closefile
Definitions: 1
Referenced from:
improperfilecmd
closegoal
Definitions: 1
Referenced from:
properproofcmd
closetheory
Definitions: 1
Referenced from:
properfilecmd
comment
Definitions: 1
Referenced from:
properproofcmd
commentdelimiter
Definitions: 1
Referenced from:
lexicalstructure
completed_attr
Definitions: 1
componentconnect
Definitions: 1
Referenced from:
componentspec
connectbyproxy
componentid_attr
Definitions: 1
componentname_attr
Definitions: 1
Referenced from:
activecompspec
componentspec
componentsocket
Definitions: 1
Referenced from:
componentconnect
componentspec
Definitions: 1
Referenced from:
launchcomp
pgipconfig
componentstatus_attr
Definitions: 1
Referenced from:
compstatus
componentsubprocess
Definitions: 1
Referenced from:
componentconnect
componenttype
Definitions: 1
Referenced from:
activecompspec
componentspec
compstatus
Definitions: 1
Referenced from:
internalmsg
connectbyproxy
Definitions: 1
Referenced from:
componentconnect
contains
Definitions: 1
Referenced from:
objtype
context_attr
Definitions: 1
Referenced from:
idtable
createobj
Definitions: 1
Referenced from:
dispobjcmd
datetime_attr
Definitions: 1
Referenced from:
filestatus
default_attr
Definitions: 1
Referenced from:
haspref
delids
Definitions: 1
Referenced from:
kitconfig
delobj
Definitions: 1
Referenced from:
dispobjmsg
replaceobjs
descr_attr
Definitions: 1
dir_attr
Definitions: 1
Not referenced from any pattern
directive
Definitions: 1
Referenced from:
litcomment
discardfile
Definitions: 1
Referenced from:
dispfilecmd
dispcmd
Definitions: 1
Referenced from:
fromdisplaymsg
dispfilecmd
Definitions: 1
Referenced from:
dispcmd
dispfilemsg
Definitions: 1
Referenced from:
dispmsg
display_attr
Definitions: 1
Referenced from:
openblock
displaycomponent
Definitions: 1
Referenced from:
componenttype
displayconfig
Definitions: 1
Referenced from:
start
kitconfig
dispmsg
Definitions: 1
Referenced from:
todisplaymsg
dispobjcmd
Definitions: 1
Referenced from:
dispcmd
dispobjmsg
Definitions: 1
Referenced from:
dispmsg
dispopenfile
Definitions: 1
Referenced from:
dispfilecmd
doccomment
Definitions: 1
Referenced from:
properproofcmd
doitem
Definitions: 1
Referenced from:
improperfilecmd
dostep
Definitions: 1
Referenced from:
improperproofcmd
editobj
Definitions: 1
Referenced from:
dispobjcmd
embed
Definitions: 1
Referenced from:
term
errorresponse
Definitions: 1
escapecharacter
Definitions: 1
Referenced from:
lexicalstructure
exitprover
Definitions: 1
Referenced from:
brokercontrol
family_attr
Definitions: 1
Referenced from:
symconfig
fatality
Definitions: 1
Referenced from:
errorresponse
field
Definitions: 1
Referenced from:
inputform
fileinfomsg
Definitions: 1
Referenced from:
fromprovermsg
filenameextns_attr
Definitions: 1
Referenced from:
proverinfo
filestatus
Definitions: 1
Referenced from:
dispfilemsg
fileurl
Definitions: 1
Referenced from:
setrefs
flagname_attr
Definitions: 1
Referenced from:
setproverflag
fold_attr
Definitions: 1
Referenced from:
openblock
forget
Definitions: 1
Referenced from:
improperproofcmd
format_attr
Definitions: 1
Referenced from:
litcomment
setformat
fromdisplaymsg
Definitions: 1
Referenced from:
pgip
fromprovermsg
Definitions: 1
Referenced from:
pgip
getpref
Definitions: 1
Referenced from:
proverconfig
giveupgoal
Definitions: 1
Referenced from:
properproofcmd
groupdelimiter
Definitions: 1
Referenced from:
properscriptcmd
haspref
Definitions: 1
Referenced from:
hasprefs
hasprefs
Definitions: 1
Referenced from:
kitconfig
objtype
helpdoc
Definitions: 1
Referenced from:
displayconfig
proverinfo
html_attr
Definitions: 1
Referenced from:
symconfig
icon
Definitions: 1
identifier
Definitions: 1
Referenced from:
idtable
identifiersyntax
Definitions: 1
Referenced from:
lexicalstructure
idtable
Definitions: 1
Referenced from:
addids
delids
setids
setrefs
idvalue
Definitions: 1
Referenced from:
kitconfig
improper_attr
Definitions: 1
Referenced from:
inputcmd
opn
improperfilecmd
Definitions: 1
Referenced from:
toprovermsg
improperproofcmd
Definitions: 1
Referenced from:
toprovermsg
indent_att
Definitions: 1
Referenced from:
box
break
indent_attr
Definitions: 1
Referenced from:
openblock
informfileloaded
Definitions: 1
Referenced from:
fileinfomsg
informfilelocation
Definitions: 1
Not referenced from any pattern
informfileoutdated
Definitions: 1
Not referenced from any pattern
informfileretracted
Definitions: 1
Referenced from:
fileinfomsg
informguise
Definitions: 1
Referenced from:
fileinfomsg
inputcmd
Definitions: 1
Referenced from:
dispobjcmd
inputform
Definitions: 1
Referenced from:
opn
instance_attr
Definitions: 1
Referenced from:
proverinfo
internalmsg
Definitions: 1
Referenced from:
pgip
interruptlevel_attr
Definitions: 1
Referenced from:
interruptprover
interruptprover
Definitions: 1
Referenced from:
dispobjcmd
keyword
Definitions: 1
Referenced from:
lexicalstructure
kind_attr
Definitions: 1
Referenced from:
atom
kitconfig
Definitions: 1
Referenced from:
fromprovermsg
knownprover
Definitions: 1
Referenced from:
knownprovers
knownprovers
Definitions: 1
Referenced from:
brokerstatus
launchcomp
Definitions: 1
Referenced from:
internalmsg
launchprover
Definitions: 1
Referenced from:
brokercontrol
lexicalstructure
Definitions: 1
Referenced from:
displayconfig
proverinfo
listwithsep_attr
Definitions: 1
Referenced from:
opsrc
litcomment
Definitions: 1
Referenced from:
properproofcmd
loadfile
Definitions: 1
Referenced from:
improperfilecmd
loadparsefile
Definitions: 1
Referenced from:
dispfilecmd
location_attrs
Definitions: 1
longhelp
Definitions: 1
Referenced from:
keyword
mandatory_attr
Definitions: 1
Referenced from:
break
max_attr
Definitions: 1
Referenced from:
pgipint
menuadd
Definitions: 1
Referenced from:
kitconfig
menudel
Definitions: 1
Referenced from:
kitconfig
metainfo
Definitions: 1
metainforesponse
Definitions: 1
Referenced from:
proveroutput
metavarid_attr
Definitions: 1
Referenced from:
openblock
scriptinsert
min_attr
Definitions: 1
Referenced from:
pgipint
name_attr
Definitions: 1
newfile
Definitions: 1
Referenced from:
dispfilemsg
newfilewith
Definitions: 1
Referenced from:
dispfilecmd
newobj
Definitions: 1
Referenced from:
dispobjmsg
replaceobjs
newprovermsg
Definitions: 1
Referenced from:
brokermsg
newstatus_attr
Definitions: 1
Referenced from:
filestatus
nonscripting
Definitions: 1
Not referenced from any pattern
normalresponse
Definitions: 1
Referenced from:
proveroutput
objectstate
Definitions: 1
Referenced from:
dispobjmsg
objid
Definitions: 1
objid_attr
Definitions: 1
objname
Definitions: 1
Not referenced from any pattern
objnames
Definitions: 1
Referenced from:
parentnames_attr
objprefval
Definitions: 1
Not referenced from any pattern
objstate
Definitions: 1
Referenced from:
newobj
objectstate
setobjstate
objtype
Definitions: 1
Referenced from:
displayconfig
objtype_attr
Definitions: 1
opcmd
Definitions: 1
Referenced from:
opn
openblock
Definitions: 1
Referenced from:
groupdelimiter
openfile
Definitions: 1
Referenced from:
improperfilecmd
opengoal
Definitions: 1
Referenced from:
properproofcmd
opentheory
Definitions: 1
Referenced from:
properfilecmd
opn
Definitions: 1
Referenced from:
displayconfig
opn_attr
Definitions: 1
Referenced from:
menuadd
opsrc
Definitions: 1
Referenced from:
opn
optrg
Definitions: 1
Referenced from:
opn
orient_attr
Definitions: 1
Referenced from:
box
othercomponent
Definitions: 1
Referenced from:
componenttype
parentnames_attr
Definitions: 1
Referenced from:
opentheory
parsercomponent
Definitions: 1
Referenced from:
componenttype
parseresult
Definitions: 1
Referenced from:
proveroutput
parsescript
Definitions: 1
Referenced from:
proofctxt
path_attr
Definitions: 1
Referenced from:
menuadd
menudel
pgip
Definitions: 1
Referenced from:
start
pgips
pgip_attrs
Definitions: 1
Referenced from:
pgip
pgip_class
Definitions: 1
Referenced from:
pgip_attrs
pgipbool
Definitions: 1
Referenced from:
pgiptype
pgipchoice
Definitions: 1
Referenced from:
pgiptype
pgipconfig
Definitions: 1
Referenced from:
start
brokercontrol
pgipconst
Definitions: 1
Referenced from:
pgiptype
pgipdoc
Definitions: 1
Referenced from:
start
pgipint
Definitions: 1
Referenced from:
pgiptype
pgipnull
Definitions: 1
Referenced from:
pgiptype
pgips
Definitions: 1
Referenced from:
start
pgipstring
Definitions: 1
Referenced from:
pgiptype
pgiptype
Definitions: 1
Referenced from:
field
haspref
pgipchoice
pgipvalue
Definitions: 1
Referenced from:
prefval
setpref
pgml
Definitions: 1
pgml_version_attr
Definitions: 1
Referenced from:
pgml
pgmlconfig
Definitions: 1
Referenced from:
kitconfig
pgmlconfiguration
Definitions: 1
Referenced from:
pgmlconfig
positionid_attr
Definitions: 1
Referenced from:
openblock
postponegoal
Definitions: 1
Referenced from:
properproofcmd
pragma
Definitions: 1
Referenced from:
properproofcmd
prefcat_attr
Definitions: 1
prefval
Definitions: 1
Referenced from:
kitconfig
prompt_attr
Definitions: 1
Referenced from:
opsrc
proofctxt
Definitions: 1
Referenced from:
directive
toprovermsg
proofpos_attr
Definitions: 1
Referenced from:
informguise
proofstep
Definitions: 1
Referenced from:
properproofcmd
properfilecmd
Definitions: 1
Referenced from:
properscriptcmd
toprovermsg
properproofcmd
Definitions: 1
Referenced from:
properscriptcmd
toprovermsg
properscriptcmd
Definitions: 1
properscriptcmdmetainfo
Definitions: 1
Referenced from:
pgipdoc
proveravailmsg
Definitions: 1
Referenced from:
brokermsg
provercomponent
Definitions: 1
Referenced from:
componenttype
proverconfig
Definitions: 1
Referenced from:
toprovermsg
provercontrol
Definitions: 1
Referenced from:
toprovermsg
proverexit
Definitions: 1
Referenced from:
provercontrol
proverid
Definitions: 1
Referenced from:
proverid_attr
proverid_attr
Definitions: 1
proverinfo
Definitions: 1
Referenced from:
kitconfig
proverinit
Definitions: 1
Referenced from:
provercontrol
provername
Definitions: 1
provername_attr
Definitions: 1
proveroutput
Definitions: 1
Referenced from:
fromprovermsg
proversquery
Definitions: 1
Referenced from:
brokercontrol
proverstate
Definitions: 1
Referenced from:
proverstatemsg
proverstatemsg
Definitions: 1
Referenced from:
brokermsg
ready
Definitions: 1
Referenced from:
proveroutput
redoitem
Definitions: 1
Referenced from:
improperfilecmd
redostep
Definitions: 1
Referenced from:
improperproofcmd
registercomp
Definitions: 1
Referenced from:
internalmsg
replaceobjs
Definitions: 1
Referenced from:
dispobjmsg
restartprover
Definitions: 1
Referenced from:
brokercontrol
restoregoal
Definitions: 1
Referenced from:
improperproofcmd
retractfile
Definitions: 1
Referenced from:
improperfilecmd
retracttheory
Definitions: 1
Referenced from:
improperfilecmd
runningprover
Definitions: 1
Referenced from:
runningprovers
runningprovers
Definitions: 1
Referenced from:
brokerstatus
saction_attr
Definitions: 1
Referenced from:
subterm
savefile
Definitions: 1
Referenced from:
dispfilecmd
scriptinsert
Definitions: 1
Referenced from:
proveroutput
scriptmarkup
Definitions: 1
sdec_attr
Definitions: 1
Referenced from:
subterm
searchtheorems
Definitions: 1
Referenced from:
proofctxt
selnumber_attr
Definitions: 1
Referenced from:
opsrc
setformat
Definitions: 1
Referenced from:
pragma
setids
Definitions: 1
Referenced from:
kitconfig
setlinewidth
Definitions: 1
Referenced from:
proofctxt
setobjstate
Definitions: 1
Referenced from:
dispobjcmd
setpref
Definitions: 1
Referenced from:
proverconfig
setproverflag
Definitions: 1
Referenced from:
provercontrol
setrefs
Definitions: 1
Not referenced from any pattern
shortcut_attr
Definitions: 1
Referenced from:
symconfig
shorthelp
Definitions: 1
Referenced from:
keyword
showctxt
Definitions: 1
Referenced from:
proofctxt
showhidecode
Definitions: 1
Referenced from:
pragma
showid
Definitions: 1
Referenced from:
proofctxt
showproofstate
Definitions: 1
Referenced from:
proofctxt
shutdownbroker
Definitions: 1
Referenced from:
brokercontrol
singleparseresult
Definitions: 1
Referenced from:
parseresult
singlepgipelem
Definitions: 1
Referenced from:
acceptedpgipelems
skind_attr
Definitions: 1
Referenced from:
subterm
sname_attr
Definitions: 1
Referenced from:
subterm
sobjtype_attr
Definitions: 1
Referenced from:
subterm
sparam_attr
Definitions: 1
Referenced from:
subterm
splace_attr
Definitions: 1
Referenced from:
subterm
spos_attr
Definitions: 1
Referenced from:
subterm
spuriouscmd
Definitions: 1
Referenced from:
properproofcmd
srcid_attr
Definitions: 1
sref_attr
Definitions: 1
Referenced from:
subterm
startupattrs
Definitions: 1
Referenced from:
componentspec
stopcomp
Definitions: 1
Referenced from:
internalmsg
stringdelimiter
Definitions: 1
Referenced from:
lexicalstructure
subterm
Definitions: 1
Referenced from:
term
sym
Definitions: 1
Referenced from:
atom
term
symconfig
Definitions: 1
Referenced from:
pgmlconfiguration
symname_attr
Definitions: 1
Referenced from:
sym
symconfig
systemattrs
Definitions: 1
Referenced from:
activecompspec
componentspec
systemcmd
Definitions: 1
Referenced from:
improperfilecmd
systemdata_attr
Definitions: 1
Referenced from:
parseresult
parsescript
systemid_attr
Definitions: 1
Referenced from:
pgml
term
Definitions: 1
Referenced from:
alt
box
pgml
subterm
textalt_attr
Definitions: 1
Referenced from:
symconfig
theoryitem
Definitions: 1
Referenced from:
properfilecmd
thmname_attr
Definitions: 1
thyname_attr
Definitions: 1
times_attr
Definitions: 1
todisplaymsg
Definitions: 1
Referenced from:
pgip
token_attr
Definitions: 1
Referenced from:
symconfig
toprovermsg
Definitions: 1
Referenced from:
pgip
undoitem
Definitions: 1
Referenced from:
improperfilecmd
undostep
Definitions: 1
Referenced from:
improperproofcmd
unicode_attr
Definitions: 1
Referenced from:
symconfig
unparseable
Definitions: 1
Referenced from:
newobj
singleparseresult
url_attr
Definitions: 1
usespgip
Definitions: 1
Referenced from:
kitconfig
usespgml
Definitions: 1
Referenced from:
kitconfig
val_attr
Definitions: 1
Referenced from:
objprefval
value
Definitions: 1
Referenced from:
metainforesponse
version_attr
Definitions: 1
Referenced from:
proverinfo
usespgip
usespgml
viewdoc
Definitions: 1
Referenced from:
proofctxt
welcomemsg
Definitions: 1
Referenced from:
displayconfig
proverinfo
whitespace
Definitions: 1
Referenced from:
properproofcmd
xmlrender
Definitions: 1
Referenced from:
symconfig