5 PGIP abstraction: document markup for proof scripts (in progress). |
5 PGIP abstraction: document markup for proof scripts (in progress). |
6 *) |
6 *) |
7 |
7 |
8 signature PGIPMARKUP = |
8 signature PGIPMARKUP = |
9 sig |
9 sig |
10 val markup_elements : string list |
10 (* Generic markup on sequential, non-overlapping pieces of proof text *) |
|
11 datatype pgipdoc = |
|
12 Openblock of { metavarid: string option } |
|
13 | Closeblock of { } |
|
14 | Opentheory of { thyname: string option, parentnames: string list , text: string} |
|
15 | Theoryitem of { name: string option, objtype: string option, text: string } |
|
16 | Closetheory of { text: string } |
|
17 | Opengoal of { thmname: string option, text: string } |
|
18 | Proofstep of { text: string } |
|
19 | Closegoal of { text: string } |
|
20 | Giveupgoal of { text: string } |
|
21 | Postponegoal of { text: string } |
|
22 | Comment of { text: string } |
|
23 | Doccomment of { text: string } |
|
24 | Whitespace of { text: string } |
|
25 | Spuriouscmd of { text: string } |
|
26 | Badcmd of { text: string } |
|
27 | Metainfo of { name: string option, text: string } |
|
28 (* Last three for PGIP literate markup only: *) |
|
29 | Litcomment of { format: string option, content: XML.content } |
|
30 | Showcode of { show: bool } |
|
31 | Setformat of { format: string } |
|
32 |
|
33 type pgipdocument = pgipdoc list |
|
34 type pgip_parser = string -> pgipdocument (* system must provide a parser P *) |
|
35 val unparse_doc : pgipdocument -> string list (* s.t. unparse (P x) = x *) |
|
36 val output_doc : pgipdocument -> XML.content |
|
37 val doc_markup_elements : string list (* used in pgip_input *) |
|
38 val doc_markup_elements_ignored : string list (* used in pgip_input *) |
11 end |
39 end |
|
40 |
12 |
41 |
13 structure PgipMarkup : PGIPMARKUP = |
42 structure PgipMarkup : PGIPMARKUP = |
14 struct |
43 struct |
|
44 open PgipTypes |
|
45 |
|
46 datatype pgipdoc = |
|
47 Openblock of { metavarid: string option } |
|
48 | Closeblock of { } |
|
49 | Opentheory of { thyname: string option, parentnames: string list , text: string} |
|
50 | Theoryitem of { name: string option, objtype: string option, text: string } |
|
51 | Closetheory of { text: string } |
|
52 | Opengoal of { thmname: string option, text: string } |
|
53 | Proofstep of { text: string } |
|
54 | Closegoal of { text: string } |
|
55 | Giveupgoal of { text: string } |
|
56 | Postponegoal of { text: string } |
|
57 | Comment of { text: string } |
|
58 | Doccomment of { text: string } |
|
59 | Whitespace of { text: string } |
|
60 | Spuriouscmd of { text: string } |
|
61 | Badcmd of { text: string } |
|
62 | Metainfo of { name: string option, text: string } |
|
63 | Litcomment of { format: string option, content: XML.content } |
|
64 | Showcode of { show: bool } |
|
65 | Setformat of { format: string } |
|
66 |
|
67 type pgipdocument = pgipdoc list |
|
68 type pgip_parser = string -> pgipdocument |
|
69 |
|
70 fun xml_of docelt = |
|
71 case docelt of |
|
72 |
|
73 Openblock vs => |
|
74 XML.Elem("openblock", opt_attr "metavarid" (#metavarid vs), []) |
|
75 |
|
76 | Closeblock vs => |
|
77 XML.Elem("closeblock", [], []) |
|
78 |
|
79 | Theoryitem vs => |
|
80 XML.Elem("theoryitem", |
|
81 opt_attr "name" (#name vs) @ |
|
82 opt_attr "objtype" (#objtype vs), |
|
83 [XML.Text (#text vs)]) |
|
84 |
|
85 | Closetheory vs => |
|
86 XML.Elem("closetheory", [], [XML.Text (#text vs)]) |
|
87 |
|
88 | Opengoal vs => |
|
89 XML.Elem("opengoal", |
|
90 opt_attr "thmname" (#thmname vs), |
|
91 [XML.Text (#text vs)]) |
|
92 |
|
93 | Proofstep vs => |
|
94 XML.Elem("proofstep", [], [XML.Text (#text vs)]) |
|
95 |
|
96 | Closegoal vs => |
|
97 XML.Elem("closegoal", [], [XML.Text (#text vs)]) |
|
98 |
|
99 | Giveupgoal vs => |
|
100 XML.Elem("giveupgoal", [], [XML.Text (#text vs)]) |
|
101 |
|
102 | Postponegoal vs => |
|
103 XML.Elem("postponegoal", [], [XML.Text (#text vs)]) |
|
104 |
|
105 | Comment vs => |
|
106 XML.Elem("comment", [], [XML.Text (#text vs)]) |
|
107 |
|
108 | Doccomment vs => |
|
109 XML.Elem("doccomment", [], [XML.Text (#text vs)]) |
|
110 |
|
111 | Spuriouscmd vs => |
|
112 XML.Elem("spuriouscmd", [], [XML.Text (#text vs)]) |
|
113 |
|
114 | Badcmd vs => |
|
115 XML.Elem("badcmd", [], [XML.Text (#text vs)]) |
|
116 |
|
117 | Metainfo vs => |
|
118 XML.Elem("metainfo", opt_attr "name" (#name vs), |
|
119 [XML.Text (#text vs)]) |
|
120 |
|
121 | Litcomment vs => |
|
122 XML.Elem("litcomment", opt_attr "format" (#format vs), |
|
123 #content vs) |
|
124 |
|
125 | Showcode vs => |
|
126 XML.Elem("showcode", |
|
127 attr "show" (PgipTypes.bool_to_pgstring (#show vs)), []) |
|
128 |
|
129 | Setformat vs => |
|
130 XML.Elem("setformat", attr "format" (#format vs), []) |
|
131 |
|
132 val output_doc = map xml_of |
|
133 |
|
134 fun unparse_elt docelt = |
|
135 case docelt of |
|
136 Openblock vs => "" |
|
137 | Closeblock vs => "" |
|
138 | Opentheory vs => #text vs |
|
139 | Theoryitem vs => #text vs |
|
140 | Closetheory vs => #text vs |
|
141 | Opengoal vs => #text vs |
|
142 | Proofstep vs => #text vs |
|
143 | Closegoal vs => #text vs |
|
144 | Giveupgoal vs => #text vs |
|
145 | Postponegoal vs => #text vs |
|
146 | Comment vs => #text vs |
|
147 | Doccomment vs => #text vs |
|
148 | Whitespace vs => #text vs |
|
149 | Spuriouscmd vs => #text vs |
|
150 | Badcmd vs => #text vs |
|
151 | Metainfo vs => #text vs |
|
152 | _ => "" |
|
153 |
|
154 |
|
155 val unparse_doc = map unparse_elt |
|
156 |
|
157 |
15 (* Names of all PGIP document markup elements *) |
158 (* Names of all PGIP document markup elements *) |
16 val markup_elements = |
159 val doc_markup_elements = |
17 [ |
160 ["openblock", |
|
161 "closeblock", |
18 "opengoal", |
162 "opengoal", |
19 "proofstep", |
163 "proofstep", |
20 "closegoal", |
164 "closegoal", |
21 "comment", |
165 "comment", |
22 "doccomment", |
166 "doccomment", |