author | chaieb |
Wed, 31 Oct 2007 12:19:41 +0100 | |
changeset 25252 | 833abbc3e733 |
parent 24584 | 01e83ffa6c54 |
child 26548 | 41bbcaf3e481 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Pure/ProofGeneral/pgml.ML |
23571 | 2 |
ID: $Id$ |
3 |
Author: David Aspinall |
|
4 |
||
5 |
PGIP abstraction: PGML |
|
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 |
||
16 |
datatype pgmlplace = Subscript | Superscript | Above | Below |
|
17 |
||
18 |
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
|
19 |
||
20 |
datatype pgmlaction = Toggle | Button | Menu |
|
21 |
||
22 |
datatype pgmlterm = |
|
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 } |
|
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
|
36 |
| Embed of XML.content |
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
|
37 |
| Raw of XML.tree |
23571 | 38 |
|
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
|
39 |
datatype pgml = |
23571 | 40 |
Pgml of { version: string option, systemid: string option, |
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
|
41 |
area: PgipTypes.displayarea option, |
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
|
42 |
content: pgmlterm list } |
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
|
43 |
|
23571 | 44 |
val pgmlterm_to_xml : pgmlterm -> XML.tree |
45 |
||
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
|
46 |
val pgml_to_xml : pgml -> XML.tree |
23571 | 47 |
end |
48 |
||
49 |
||
50 |
structure Pgml : PGML = |
|
51 |
struct |
|
52 |
open PgipTypes |
|
53 |
||
54 |
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
|
55 |
|
23571 | 56 |
datatype pgmlatom = Sym of pgmlsym | Str of string |
57 |
||
58 |
datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient |
|
59 |
||
60 |
datatype pgmlplace = Subscript | Superscript | Above | Below |
|
61 |
||
62 |
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string |
|
63 |
||
64 |
datatype pgmlaction = Toggle | Button | Menu |
|
65 |
||
66 |
datatype pgmlterm = |
|
67 |
Atoms of { kind: string option, content: pgmlatom list } |
|
68 |
| Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list } |
|
69 |
| Break of { mandatory: bool option, indent: int option } |
|
70 |
| Subterm of { kind: string option, |
|
71 |
param: string option, |
|
72 |
place: pgmlplace option, |
|
73 |
name: string option, |
|
74 |
decoration: pgmldec option, |
|
75 |
action: pgmlaction option, |
|
76 |
pos: string option, |
|
77 |
xref: PgipTypes.pgipurl option, |
|
78 |
content: pgmlterm list } |
|
79 |
| Alt of { kind: string option, 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
|
80 |
| Embed of XML.content |
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
|
81 |
| Raw of XML.tree |
23571 | 82 |
|
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
|
83 |
|
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
|
84 |
datatype pgml = |
23571 | 85 |
Pgml of { version: string option, systemid: string option, |
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
|
86 |
area: PgipTypes.displayarea option, |
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
|
87 |
content: pgmlterm list } |
23571 | 88 |
|
89 |
fun pgmlorient_to_string HOVOrient = "hov" |
|
90 |
| pgmlorient_to_string HOrient = "h" |
|
91 |
| pgmlorient_to_string VOrient = "v" |
|
92 |
| pgmlorient_to_string HVOrient = "hv" |
|
93 |
||
94 |
fun pgmlplace_to_string Subscript = "sub" |
|
95 |
| pgmlplace_to_string Superscript = "sup" |
|
96 |
| pgmlplace_to_string Above = "above" |
|
97 |
| pgmlplace_to_string Below = "below" |
|
98 |
||
99 |
fun pgmldec_to_string Bold = "bold" |
|
100 |
| pgmldec_to_string Italic = "italic" |
|
101 |
| pgmldec_to_string Error = "error" |
|
102 |
| pgmldec_to_string Warning = "warning" |
|
103 |
| pgmldec_to_string Info = "info" |
|
104 |
| pgmldec_to_string (Other s) = "other" |
|
105 |
||
106 |
fun pgmlaction_to_string Toggle = "toggle" |
|
107 |
| pgmlaction_to_string Button = "button" |
|
108 |
| pgmlaction_to_string Menu = "menu" |
|
109 |
||
23610 | 110 |
(* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle; |
111 |
would be better not to *) |
|
23723 | 112 |
fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content]) |
113 |
| atom_to_xml (Str str) = XML.Output str |
|
23571 | 114 |
|
115 |
fun pgmlterm_to_xml (Atoms {kind, content}) = |
|
116 |
XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content) |
|
117 |
||
118 |
| pgmlterm_to_xml (Box {orient, indent, content}) = |
|
119 |
XML.Elem("box", |
|
120 |
opt_attr_map pgmlorient_to_string "orient" orient @ |
|
121 |
opt_attr_map int_to_pgstring "indent" indent, |
|
122 |
map pgmlterm_to_xml content) |
|
123 |
||
124 |
| pgmlterm_to_xml (Break {mandatory, indent}) = |
|
125 |
XML.Elem("break", |
|
126 |
opt_attr_map bool_to_pgstring "mandatory" mandatory @ |
|
127 |
opt_attr_map int_to_pgstring "indent" indent, []) |
|
128 |
||
129 |
| pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) = |
|
130 |
XML.Elem("subterm", |
|
131 |
opt_attr "kind" kind @ |
|
132 |
opt_attr "param" param @ |
|
133 |
opt_attr_map pgmlplace_to_string "place" place @ |
|
134 |
opt_attr "name" name @ |
|
135 |
opt_attr_map pgmldec_to_string "decoration" decoration @ |
|
136 |
opt_attr_map pgmlaction_to_string "action" action @ |
|
137 |
opt_attr "pos" pos @ |
|
138 |
opt_attr_map string_of_pgipurl "xref" xref, |
|
139 |
map pgmlterm_to_xml content) |
|
140 |
||
141 |
| pgmlterm_to_xml (Alt {kind, content}) = |
|
142 |
XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content) |
|
143 |
||
144 |
| pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls) |
|
145 |
||
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
|
146 |
| pgmlterm_to_xml (Raw xml) = xml |
23571 | 147 |
|
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
|
148 |
|
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 |
datatype pgml = |
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
|
150 |
Pgml of { version: string option, systemid: string option, |
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
|
151 |
area: PgipTypes.displayarea option, |
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
|
152 |
content: pgmlterm list } |
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
|
153 |
|
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 |
fun pgml_to_xml (Pgml {version,systemid,area,content}) = |
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
|
155 |
XML.Elem("pgml", |
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
|
156 |
opt_attr "version" version @ |
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
|
157 |
opt_attr "systemid" systemid @ |
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
|
158 |
Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]), |
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
|
159 |
map pgmlterm_to_xml content) |
23571 | 160 |
end |