--- a/src/Pure/ProofGeneral/pgml.ML Thu Aug 28 00:33:17 2008 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML Thu Aug 28 00:33:19 2008 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: David Aspinall
-PGIP abstraction: PGML
+PGIP abstraction: PGML
*)
signature PGML =
@@ -13,13 +13,13 @@
datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
- datatype pgmlplace = Subscript | Superscript | Above | Below
+ datatype pgmlplace = Subscript | Superscript | Above | Below
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
datatype pgmlaction = Toggle | Button | Menu
-
- datatype pgmlterm =
+
+ datatype pgmlterm =
Atoms of { kind: string option, content: pgmlatom list }
| Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
| Break of { mandatory: bool option, indent: int option }
@@ -36,11 +36,12 @@
| Embed of XML.tree list
| Raw of XML.tree
- datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
+ datatype pgml =
+ Pgml of { version: string option, systemid: string option,
+ area: PgipTypes.displayarea option,
content: pgmlterm list }
-
+
+ val atom_to_xml : pgmlatom -> XML.tree
val pgmlterm_to_xml : pgmlterm -> XML.tree
val pgml_to_xml : pgml -> XML.tree
@@ -57,13 +58,13 @@
datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
- datatype pgmlplace = Subscript | Superscript | Above | Below
+ datatype pgmlplace = Subscript | Superscript | Above | Below
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
datatype pgmlaction = Toggle | Button | Menu
-
- datatype pgmlterm =
+
+ datatype pgmlterm =
Atoms of { kind: string option, content: pgmlatom list }
| Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
| Break of { mandatory: bool option, indent: int option }
@@ -80,10 +81,10 @@
| Embed of XML.tree list
| Raw of XML.tree
-
- datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
+
+ datatype pgml =
+ Pgml of { version: string option, systemid: string option,
+ area: PgipTypes.displayarea option,
content: pgmlterm list }
fun pgmlorient_to_string HOVOrient = "hov"
@@ -107,16 +108,16 @@
| pgmlaction_to_string Button = "button"
| pgmlaction_to_string Menu = "menu"
- (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
- would be better not to *)
- fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
- | atom_to_xml (Str str) = XML.Output str
-
- fun pgmlterm_to_xml (Atoms {kind, content}) =
- XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
+ (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
+ would be better not to *) (* FIXME !??? *)
+ fun atom_to_xml (Sym {name, content}) = XML.Elem ("sym", attr name name, [XML.Text content])
+ | atom_to_xml (Str content) = XML.Text content;
+
+ fun pgmlterm_to_xml (Atoms {kind, content}) =
+ XML.Elem("atom", opt_attr "kind" kind, map atom_to_xml content)
| pgmlterm_to_xml (Box {orient, indent, content}) =
- XML.Elem("box",
+ XML.Elem("box",
opt_attr_map pgmlorient_to_string "orient" orient @
opt_attr_map int_to_pgstring "indent" indent,
map pgmlterm_to_xml content)
@@ -127,18 +128,18 @@
opt_attr_map int_to_pgstring "indent" indent, [])
| pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
- XML.Elem("subterm",
+ XML.Elem("subterm",
opt_attr "kind" kind @
opt_attr "param" param @
opt_attr_map pgmlplace_to_string "place" place @
- opt_attr "name" name @
+ opt_attr "name" name @
opt_attr_map pgmldec_to_string "decoration" decoration @
- opt_attr_map pgmlaction_to_string "action" action @
+ opt_attr_map pgmlaction_to_string "action" action @
opt_attr "pos" pos @
opt_attr_map string_of_pgipurl "xref" xref,
map pgmlterm_to_xml content)
- | pgmlterm_to_xml (Alt {kind, content}) =
+ | pgmlterm_to_xml (Alt {kind, content}) =
XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
| pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
@@ -146,14 +147,14 @@
| pgmlterm_to_xml (Raw xml) = xml
- datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
+ datatype pgml =
+ Pgml of { version: string option, systemid: string option,
+ area: PgipTypes.displayarea option,
content: pgmlterm list }
- fun pgml_to_xml (Pgml {version,systemid,area,content}) =
+ fun pgml_to_xml (Pgml {version,systemid,area,content}) =
XML.Elem("pgml",
- opt_attr "version" version @
+ opt_attr "version" version @
opt_attr "systemid" systemid @
Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
map pgmlterm_to_xml content)