1.1 --- a/src/Pure/ProofGeneral/pgml.ML Wed Aug 27 11:49:50 2008 +0200
1.2 +++ b/src/Pure/ProofGeneral/pgml.ML Wed Aug 27 12:00:28 2008 +0200
1.3 @@ -18,29 +18,29 @@
1.4 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
1.5
1.6 datatype pgmlaction = Toggle | Button | Menu
1.7 -
1.8 +
1.9 datatype pgmlterm =
1.10 - Atoms of { kind: string option, content: pgmlatom list }
1.11 - | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
1.12 - | Break of { mandatory: bool option, indent: int option }
1.13 - | Subterm of { kind: string option,
1.14 - param: string option,
1.15 - place: pgmlplace option,
1.16 - name: string option,
1.17 - decoration: pgmldec option,
1.18 - action: pgmlaction option,
1.19 - pos: string option,
1.20 - xref: PgipTypes.pgipurl option,
1.21 - content: pgmlterm list }
1.22 - | Alt of { kind: string option, content: pgmlterm list }
1.23 - | Embed of XML.tree list
1.24 - | Raw of XML.tree
1.25 + Atoms of { kind: string option, content: pgmlatom list }
1.26 + | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
1.27 + | Break of { mandatory: bool option, indent: int option }
1.28 + | Subterm of { kind: string option,
1.29 + param: string option,
1.30 + place: pgmlplace option,
1.31 + name: string option,
1.32 + decoration: pgmldec option,
1.33 + action: pgmlaction option,
1.34 + pos: string option,
1.35 + xref: PgipTypes.pgipurl option,
1.36 + content: pgmlterm list }
1.37 + | Alt of { kind: string option, content: pgmlterm list }
1.38 + | Embed of XML.tree list
1.39 + | Raw of XML.tree
1.40
1.41 datatype pgml =
1.42 - Pgml of { version: string option, systemid: string option,
1.43 - area: PgipTypes.displayarea option,
1.44 - content: pgmlterm list }
1.45 -
1.46 + Pgml of { version: string option, systemid: string option,
1.47 + area: PgipTypes.displayarea option,
1.48 + content: pgmlterm list }
1.49 +
1.50 val pgmlterm_to_xml : pgmlterm -> XML.tree
1.51
1.52 val pgml_to_xml : pgml -> XML.tree
1.53 @@ -62,29 +62,29 @@
1.54 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
1.55
1.56 datatype pgmlaction = Toggle | Button | Menu
1.57 -
1.58 +
1.59 datatype pgmlterm =
1.60 - Atoms of { kind: string option, content: pgmlatom list }
1.61 - | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
1.62 - | Break of { mandatory: bool option, indent: int option }
1.63 - | Subterm of { kind: string option,
1.64 - param: string option,
1.65 - place: pgmlplace option,
1.66 - name: string option,
1.67 - decoration: pgmldec option,
1.68 - action: pgmlaction option,
1.69 - pos: string option,
1.70 - xref: PgipTypes.pgipurl option,
1.71 - content: pgmlterm list }
1.72 - | Alt of { kind: string option, content: pgmlterm list }
1.73 - | Embed of XML.tree list
1.74 - | Raw of XML.tree
1.75 + Atoms of { kind: string option, content: pgmlatom list }
1.76 + | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
1.77 + | Break of { mandatory: bool option, indent: int option }
1.78 + | Subterm of { kind: string option,
1.79 + param: string option,
1.80 + place: pgmlplace option,
1.81 + name: string option,
1.82 + decoration: pgmldec option,
1.83 + action: pgmlaction option,
1.84 + pos: string option,
1.85 + xref: PgipTypes.pgipurl option,
1.86 + content: pgmlterm list }
1.87 + | Alt of { kind: string option, content: pgmlterm list }
1.88 + | Embed of XML.tree list
1.89 + | Raw of XML.tree
1.90
1.91 -
1.92 +
1.93 datatype pgml =
1.94 - Pgml of { version: string option, systemid: string option,
1.95 - area: PgipTypes.displayarea option,
1.96 - content: pgmlterm list }
1.97 + Pgml of { version: string option, systemid: string option,
1.98 + area: PgipTypes.displayarea option,
1.99 + content: pgmlterm list }
1.100
1.101 fun pgmlorient_to_string HOVOrient = "hov"
1.102 | pgmlorient_to_string HOrient = "h"
1.103 @@ -111,35 +111,35 @@
1.104 would be better not to *)
1.105 fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
1.106 | atom_to_xml (Str str) = XML.Output str
1.107 -
1.108 +
1.109 fun pgmlterm_to_xml (Atoms {kind, content}) =
1.110 - XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
1.111 + XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
1.112
1.113 | pgmlterm_to_xml (Box {orient, indent, content}) =
1.114 - XML.Elem("box",
1.115 - opt_attr_map pgmlorient_to_string "orient" orient @
1.116 - opt_attr_map int_to_pgstring "indent" indent,
1.117 - map pgmlterm_to_xml content)
1.118 + XML.Elem("box",
1.119 + opt_attr_map pgmlorient_to_string "orient" orient @
1.120 + opt_attr_map int_to_pgstring "indent" indent,
1.121 + map pgmlterm_to_xml content)
1.122
1.123 | pgmlterm_to_xml (Break {mandatory, indent}) =
1.124 - XML.Elem("break",
1.125 - opt_attr_map bool_to_pgstring "mandatory" mandatory @
1.126 - opt_attr_map int_to_pgstring "indent" indent, [])
1.127 + XML.Elem("break",
1.128 + opt_attr_map bool_to_pgstring "mandatory" mandatory @
1.129 + opt_attr_map int_to_pgstring "indent" indent, [])
1.130
1.131 | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
1.132 - XML.Elem("subterm",
1.133 - opt_attr "kind" kind @
1.134 - opt_attr "param" param @
1.135 - opt_attr_map pgmlplace_to_string "place" place @
1.136 - opt_attr "name" name @
1.137 - opt_attr_map pgmldec_to_string "decoration" decoration @
1.138 - opt_attr_map pgmlaction_to_string "action" action @
1.139 - opt_attr "pos" pos @
1.140 - opt_attr_map string_of_pgipurl "xref" xref,
1.141 - map pgmlterm_to_xml content)
1.142 + XML.Elem("subterm",
1.143 + opt_attr "kind" kind @
1.144 + opt_attr "param" param @
1.145 + opt_attr_map pgmlplace_to_string "place" place @
1.146 + opt_attr "name" name @
1.147 + opt_attr_map pgmldec_to_string "decoration" decoration @
1.148 + opt_attr_map pgmlaction_to_string "action" action @
1.149 + opt_attr "pos" pos @
1.150 + opt_attr_map string_of_pgipurl "xref" xref,
1.151 + map pgmlterm_to_xml content)
1.152
1.153 | pgmlterm_to_xml (Alt {kind, content}) =
1.154 - XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
1.155 + XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
1.156
1.157 | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
1.158
1.159 @@ -147,14 +147,14 @@
1.160
1.161
1.162 datatype pgml =
1.163 - Pgml of { version: string option, systemid: string option,
1.164 - area: PgipTypes.displayarea option,
1.165 - content: pgmlterm list }
1.166 + Pgml of { version: string option, systemid: string option,
1.167 + area: PgipTypes.displayarea option,
1.168 + content: pgmlterm list }
1.169
1.170 fun pgml_to_xml (Pgml {version,systemid,area,content}) =
1.171 - XML.Elem("pgml",
1.172 - opt_attr "version" version @
1.173 - opt_attr "systemid" systemid @
1.174 - Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
1.175 - map pgmlterm_to_xml content)
1.176 + XML.Elem("pgml",
1.177 + opt_attr "version" version @
1.178 + opt_attr "systemid" systemid @
1.179 + Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
1.180 + map pgmlterm_to_xml content)
1.181 end