Proof General PGIP/PGML Schema
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
 
alt
Definitions: 1
Referenced from:
term
altkind_attr
Definitions: 1
Referenced from:
alt
area_attr
Definitions: 1
Referenced from:
pgml
atom
Definitions: 1
Referenced from:
term
box
Definitions: 1
Referenced from:
term
break
Definitions: 1
Referenced from:
term
embed
Definitions: 1
Referenced from:
term
family_attr
Definitions: 1
Referenced from:
symconfig
html_attr
Definitions: 1
Referenced from:
symconfig
indent_att
Definitions: 1
Referenced from:
box
break
kind_attr
Definitions: 1
Referenced from:
atom
mandatory_attr
Definitions: 1
Referenced from:
break
orient_attr
Definitions: 1
Referenced from:
box
pgml
Definitions: 1
Not referenced from any pattern
pgml_version_attr
Definitions: 1
Referenced from:
pgml
pgmlconfiguration
Definitions: 1
Not referenced from any pattern
saction_attr
Definitions: 1
Referenced from:
subterm
sdec_attr
Definitions: 1
Referenced from:
subterm
shortcut_attr
Definitions: 1
Referenced from:
symconfig
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
sref_attr
Definitions: 1
Referenced from:
subterm
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
systemid_attr
Definitions: 1
Referenced from:
pgml
term
Definitions: 1
Referenced from:
alt
box
pgml
subterm
textalt_attr
Definitions: 1
Referenced from:
symconfig
token_attr
Definitions: 1
Referenced from:
symconfig
unicode_attr
Definitions: 1
Referenced from:
symconfig
xmlrender
Definitions: 1
Referenced from:
symconfig