author | wenzelm |
Sat, 13 Dec 2008 15:00:39 +0100 | |
changeset 29091 | b81fe045e799 |
parent 28039 | 4d28b4d134f6 |
child 29606 | fedb8be05f24 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Pure/ProofGeneral/pgml.ML |
23571 | 2 |
ID: $Id$ |
3 |
Author: David Aspinall |
|
4 |
||
28038 | 5 |
PGIP abstraction: PGML |
23571 | 6 |
*) |
7 |
||
8 |
signature PGML = |
|
9 |
sig |
|
10 |
type pgmlsym = { name: string, content: string } |
|
11 |
||
12 |
datatype pgmlatom = Sym of pgmlsym | Str of string |
|
13 |
||
14 |
datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient |
|
15 |
||
28038 | 16 |
datatype pgmlplace = Subscript | Superscript | Above | Below |
23571 | 17 |
|
18 |
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
|
19 |
||
20 |
datatype pgmlaction = Toggle | Button | Menu |
|
28038 | 21 |
|
22 |
datatype pgmlterm = |
|
28020 | 23 |
Atoms of { kind: string option, content: pgmlatom list } |
24 |
| Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
|
25 |
| Break of { mandatory: bool option, indent: int option } |
|
26 |
| Subterm of { kind: string option, |
|
27 |
param: string option, |
|
28 |
place: pgmlplace option, |
|
29 |
name: string option, |
|
30 |
decoration: pgmldec option, |
|
31 |
action: pgmlaction option, |
|
32 |
pos: string option, |
|
33 |
xref: PgipTypes.pgipurl option, |
|
34 |
content: pgmlterm list } |
|
35 |
| Alt of { kind: string option, content: pgmlterm list } |
|
36 |
| Embed of XML.tree list |
|
37 |
| Raw of XML.tree |
|
23571 | 38 |
|
28038 | 39 |
datatype pgml = |
40 |
Pgml of { version: string option, systemid: string option, |
|
41 |
area: PgipTypes.displayarea option, |
|
28020 | 42 |
content: pgmlterm list } |
28038 | 43 |
|
44 |
val atom_to_xml : pgmlatom -> XML.tree |
|
23571 | 45 |
val pgmlterm_to_xml : pgmlterm -> XML.tree |
46 |
||
23748
1ff6b562076f
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
aspinall
parents:
23723
diff
changeset
|
47 |
val pgml_to_xml : pgml -> XML.tree |
23571 | 48 |
end |
49 |
||
50 |
||
51 |
structure Pgml : PGML = |
|
52 |
struct |
|
53 |
open PgipTypes |
|
54 |
||
55 |
type pgmlsym = { name: string, content: string } |
|
23748
1ff6b562076f
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
aspinall
parents:
23723
diff
changeset
|
56 |
|
23571 | 57 |
datatype pgmlatom = Sym of pgmlsym | Str of string |
58 |
||
59 |
datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient |
|
60 |
||
28038 | 61 |
datatype pgmlplace = Subscript | Superscript | Above | Below |
23571 | 62 |
|
63 |
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
|
64 |
||
65 |
datatype pgmlaction = Toggle | Button | Menu |
|
28038 | 66 |
|
67 |
datatype pgmlterm = |
|
28020 | 68 |
Atoms of { kind: string option, content: pgmlatom list } |
69 |
| Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
|
70 |
| Break of { mandatory: bool option, indent: int option } |
|
71 |
| Subterm of { kind: string option, |
|
72 |
param: string option, |
|
73 |
place: pgmlplace option, |
|
74 |
name: string option, |
|
75 |
decoration: pgmldec option, |
|
76 |
action: pgmlaction option, |
|
77 |
pos: string option, |
|
78 |
xref: PgipTypes.pgipurl option, |
|
79 |
content: pgmlterm list } |
|
80 |
| Alt of { kind: string option, content: pgmlterm list } |
|
81 |
| Embed of XML.tree list |
|
82 |
| Raw of XML.tree |
|
23571 | 83 |
|
28038 | 84 |
|
85 |
datatype pgml = |
|
86 |
Pgml of { version: string option, systemid: string option, |
|
87 |
area: PgipTypes.displayarea option, |
|
28020 | 88 |
content: pgmlterm list } |
23571 | 89 |
|
90 |
fun pgmlorient_to_string HOVOrient = "hov" |
|
91 |
| pgmlorient_to_string HOrient = "h" |
|
92 |
| pgmlorient_to_string VOrient = "v" |
|
93 |
| pgmlorient_to_string HVOrient = "hv" |
|
94 |
||
95 |
fun pgmlplace_to_string Subscript = "sub" |
|
96 |
| pgmlplace_to_string Superscript = "sup" |
|
97 |
| pgmlplace_to_string Above = "above" |
|
98 |
| pgmlplace_to_string Below = "below" |
|
99 |
||
100 |
fun pgmldec_to_string Bold = "bold" |
|
101 |
| pgmldec_to_string Italic = "italic" |
|
102 |
| pgmldec_to_string Error = "error" |
|
103 |
| pgmldec_to_string Warning = "warning" |
|
104 |
| pgmldec_to_string Info = "info" |
|
105 |
| pgmldec_to_string (Other s) = "other" |
|
106 |
||
107 |
fun pgmlaction_to_string Toggle = "toggle" |
|
108 |
| pgmlaction_to_string Button = "button" |
|
109 |
| pgmlaction_to_string Menu = "menu" |
|
110 |
||
28038 | 111 |
(* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; |
112 |
would be better not to *) (* FIXME !??? *) |
|
28039 | 113 |
fun atom_to_xml (Sym {name, content}) = XML.Elem ("sym", attr "name" name, [XML.Text content]) |
28038 | 114 |
| atom_to_xml (Str content) = XML.Text content; |
115 |
||
116 |
fun pgmlterm_to_xml (Atoms {kind, content}) = |
|
117 |
XML.Elem("atom", opt_attr "kind" kind, map atom_to_xml content) |
|
23571 | 118 |
|
119 |
| pgmlterm_to_xml (Box {orient, indent, content}) = |
|
28038 | 120 |
XML.Elem("box", |
28020 | 121 |
opt_attr_map pgmlorient_to_string "orient" orient @ |
122 |
opt_attr_map int_to_pgstring "indent" indent, |
|
123 |
map pgmlterm_to_xml content) |
|
23571 | 124 |
|
125 |
| pgmlterm_to_xml (Break {mandatory, indent}) = |
|
28020 | 126 |
XML.Elem("break", |
127 |
opt_attr_map bool_to_pgstring "mandatory" mandatory @ |
|
128 |
opt_attr_map int_to_pgstring "indent" indent, []) |
|
23571 | 129 |
|
130 |
| pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) = |
|
28038 | 131 |
XML.Elem("subterm", |
28020 | 132 |
opt_attr "kind" kind @ |
133 |
opt_attr "param" param @ |
|
134 |
opt_attr_map pgmlplace_to_string "place" place @ |
|
28038 | 135 |
opt_attr "name" name @ |
28020 | 136 |
opt_attr_map pgmldec_to_string "decoration" decoration @ |
28038 | 137 |
opt_attr_map pgmlaction_to_string "action" action @ |
28020 | 138 |
opt_attr "pos" pos @ |
139 |
opt_attr_map string_of_pgipurl "xref" xref, |
|
140 |
map pgmlterm_to_xml content) |
|
23571 | 141 |
|
28038 | 142 |
| pgmlterm_to_xml (Alt {kind, content}) = |
28020 | 143 |
XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content) |
23571 | 144 |
|
145 |
| pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls) |
|
146 |
||
23748
1ff6b562076f
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
aspinall
parents:
23723
diff
changeset
|
147 |
| pgmlterm_to_xml (Raw xml) = xml |
23571 | 148 |
|
23748
1ff6b562076f
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
aspinall
parents:
23723
diff
changeset
|
149 |
|
28038 | 150 |
datatype pgml = |
151 |
Pgml of { version: string option, systemid: string option, |
|
152 |
area: PgipTypes.displayarea option, |
|
28020 | 153 |
content: pgmlterm list } |
23748
1ff6b562076f
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
aspinall
parents:
23723
diff
changeset
|
154 |
|
28038 | 155 |
fun pgml_to_xml (Pgml {version,systemid,area,content}) = |
28020 | 156 |
XML.Elem("pgml", |
28038 | 157 |
opt_attr "version" version @ |
28020 | 158 |
opt_attr "systemid" systemid @ |
159 |
Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]), |
|
160 |
map pgmlterm_to_xml content) |
|
23571 | 161 |
end |