author | wenzelm |
Fri, 27 Jul 2007 21:55:20 +0200 | |
changeset 24010 | 2ef318813e1a |
parent 23834 | ad6ad61332fa |
child 24192 | 4eccd4bb8b64 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/pgip_markup.ML |
2 |
ID: $Id$ |
|
3 |
Author: David Aspinall |
|
4 |
||
5 |
PGIP abstraction: document markup for proof scripts (in progress). |
|
6 |
*) |
|
7 |
||
8 |
signature PGIPMARKUP = |
|
9 |
sig |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
10 |
(* Generic markup on sequential, non-overlapping pieces of proof text *) |
23799 | 11 |
datatype pgipdoc = |
12 |
Openblock of { metavarid: string option, name: string option, |
|
13 |
objtype: PgipTypes.objtype option } |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
14 |
| Closeblock of { } |
21867 | 15 |
| Opentheory of { thyname: string, parentnames: string list , text: string} |
22404
790935f7c1ab
Add more attributes to openblock. Change theory item objtype field to proper objtype.
aspinall
parents:
21886
diff
changeset
|
16 |
| Theoryitem of { name: string option, objtype: PgipTypes.objtype option, text: string } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
17 |
| Closetheory of { text: string } |
23799 | 18 |
| Opengoal of { thmname: string option, text: string } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
19 |
| Proofstep of { text: string } |
23799 | 20 |
| Closegoal of { text: string } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
21 |
| Giveupgoal of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
22 |
| Postponegoal of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
23 |
| Comment of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
24 |
| Doccomment of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
25 |
| Whitespace of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
26 |
| Spuriouscmd of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
27 |
| Badcmd of { text: string } |
23799 | 28 |
| Unparseable of { text: string } |
29 |
| Metainfo of { name: string option, text: string } |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
30 |
(* Last three for PGIP literate markup only: *) |
23799 | 31 |
| Litcomment of { format: string option, content: XML.content } |
32 |
| Showcode of { show: bool } |
|
33 |
| Setformat of { format: string } |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
34 |
|
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
35 |
type pgipdocument = pgipdoc list |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
36 |
type pgip_parser = string -> pgipdocument (* system must provide a parser P *) |
23799 | 37 |
val unparse_doc : pgipdocument -> string list (* s.t. unparse (P x) = x *) |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
38 |
val output_doc : pgipdocument -> XML.content |
23799 | 39 |
val doc_markup_elements : string list (* used in pgip_input *) |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
40 |
val doc_markup_elements_ignored : string list (* used in pgip_input *) |
21637 | 41 |
end |
42 |
||
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
43 |
|
21637 | 44 |
structure PgipMarkup : PGIPMARKUP = |
45 |
struct |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
46 |
open PgipTypes |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
47 |
|
21867 | 48 |
(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *) |
23799 | 49 |
datatype pgipdoc = |
50 |
Openblock of { metavarid: string option, name: string option, |
|
51 |
objtype: PgipTypes.objtype option } |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
52 |
| Closeblock of { } |
21867 | 53 |
| Opentheory of { thyname: string, parentnames: string list, text: string} |
22404
790935f7c1ab
Add more attributes to openblock. Change theory item objtype field to proper objtype.
aspinall
parents:
21886
diff
changeset
|
54 |
| Theoryitem of { name: string option, objtype: PgipTypes.objtype option, text: string } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
55 |
| Closetheory of { text: string } |
23799 | 56 |
| Opengoal of { thmname: string option, text: string } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
57 |
| Proofstep of { text: string } |
23799 | 58 |
| Closegoal of { text: string } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
59 |
| Giveupgoal of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
60 |
| Postponegoal of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
61 |
| Comment of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
62 |
| Doccomment of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
63 |
| Whitespace of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
64 |
| Spuriouscmd of { text: string } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
65 |
| Badcmd of { text: string } |
23799 | 66 |
| Unparseable of { text: string } |
67 |
| Metainfo of { name: string option, text: string } |
|
68 |
| Litcomment of { format: string option, content: XML.content } |
|
69 |
| Showcode of { show: bool } |
|
70 |
| Setformat of { format: string } |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
71 |
|
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
72 |
type pgipdocument = pgipdoc list |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
73 |
type pgip_parser = string -> pgipdocument |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
74 |
|
23799 | 75 |
fun xml_of docelt = |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
76 |
case docelt of |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
77 |
|
23799 | 78 |
Openblock vs => |
79 |
XML.Elem("openblock", opt_attr "name" (#metavarid vs) @ |
|
80 |
opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @ |
|
81 |
opt_attr "metavarid" (#metavarid vs), |
|
82 |
[]) |
|
83 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23799
diff
changeset
|
84 |
| Closeblock _ => |
23799 | 85 |
XML.Elem("closeblock", [], []) |
86 |
||
87 |
| Opentheory vs => |
|
88 |
XML.Elem("opentheory", |
|
89 |
attr "thyname" (#thyname vs) @ |
|
90 |
opt_attr "parentnames" |
|
91 |
(case (#parentnames vs) |
|
92 |
of [] => NONE |
|
93 |
| ps => SOME (space_implode ";" ps)), |
|
94 |
[XML.Text (#text vs)]) |
|
21867 | 95 |
|
23799 | 96 |
| Theoryitem vs => |
97 |
XML.Elem("theoryitem", |
|
98 |
opt_attr "name" (#name vs) @ |
|
99 |
opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs), |
|
100 |
[XML.Text (#text vs)]) |
|
101 |
||
102 |
| Closetheory vs => |
|
103 |
XML.Elem("closetheory", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
104 |
|
23799 | 105 |
| Opengoal vs => |
106 |
XML.Elem("opengoal", |
|
107 |
opt_attr "thmname" (#thmname vs), |
|
108 |
[XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
109 |
|
23799 | 110 |
| Proofstep vs => |
111 |
XML.Elem("proofstep", [], [XML.Text (#text vs)]) |
|
112 |
||
113 |
| Closegoal vs => |
|
114 |
XML.Elem("closegoal", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
115 |
|
23799 | 116 |
| Giveupgoal vs => |
117 |
XML.Elem("giveupgoal", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
118 |
|
23799 | 119 |
| Postponegoal vs => |
120 |
XML.Elem("postponegoal", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
121 |
|
23799 | 122 |
| Comment vs => |
123 |
XML.Elem("comment", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
124 |
|
23799 | 125 |
| Whitespace vs => |
126 |
XML.Elem("whitespace", [], [XML.Text (#text vs)]) |
|
21867 | 127 |
|
23799 | 128 |
| Doccomment vs => |
129 |
XML.Elem("doccomment", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
130 |
|
23799 | 131 |
| Spuriouscmd vs => |
132 |
XML.Elem("spuriouscmd", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
133 |
|
23799 | 134 |
| Badcmd vs => |
135 |
XML.Elem("badcmd", [], [XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
136 |
|
23799 | 137 |
| Unparseable vs => |
138 |
XML.Elem("unparseable", [], [XML.Text (#text vs)]) |
|
21867 | 139 |
|
23799 | 140 |
| Metainfo vs => |
141 |
XML.Elem("metainfo", opt_attr "name" (#name vs), |
|
142 |
[XML.Text (#text vs)]) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
143 |
|
23799 | 144 |
| Litcomment vs => |
145 |
XML.Elem("litcomment", opt_attr "format" (#format vs), |
|
146 |
#content vs) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
147 |
|
23799 | 148 |
| Showcode vs => |
149 |
XML.Elem("showcode", |
|
150 |
attr "show" (PgipTypes.bool_to_pgstring (#show vs)), []) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
151 |
|
23799 | 152 |
| Setformat vs => |
153 |
XML.Elem("setformat", attr "format" (#format vs), []) |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
154 |
|
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
155 |
val output_doc = map xml_of |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
156 |
|
23799 | 157 |
fun unparse_elt docelt = |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
158 |
case docelt of |
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23799
diff
changeset
|
159 |
Openblock _ => "" |
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23799
diff
changeset
|
160 |
| Closeblock _ => "" |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
161 |
| Opentheory vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
162 |
| Theoryitem vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
163 |
| Closetheory vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
164 |
| Opengoal vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
165 |
| Proofstep vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
166 |
| Closegoal vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
167 |
| Giveupgoal vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
168 |
| Postponegoal vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
169 |
| Comment vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
170 |
| Doccomment vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
171 |
| Whitespace vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
172 |
| Spuriouscmd vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
173 |
| Badcmd vs => #text vs |
21867 | 174 |
| Unparseable vs => #text vs |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
175 |
| Metainfo vs => #text vs |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
176 |
| _ => "" |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
177 |
|
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
178 |
|
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
179 |
val unparse_doc = map unparse_elt |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
180 |
|
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
181 |
|
21637 | 182 |
(* Names of all PGIP document markup elements *) |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
183 |
val doc_markup_elements = |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
184 |
["openblock", |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
185 |
"closeblock", |
23799 | 186 |
"opentheory", |
187 |
"theoryitem", |
|
188 |
"closetheory", |
|
189 |
"opengoal", |
|
190 |
"proofstep", |
|
191 |
"closegoal", |
|
192 |
"giveupgoal", |
|
193 |
"postponegoal", |
|
194 |
"comment", |
|
195 |
"doccomment", |
|
196 |
"whitespace", |
|
197 |
"spuriouscmd", |
|
198 |
"badcmd", |
|
199 |
(* the prover shouldn't really receive the next ones, |
|
200 |
but we include them here so that they are harmlessly |
|
21886 | 201 |
ignored. *) |
23799 | 202 |
"unparseable", |
203 |
"metainfo", |
|
21886 | 204 |
(* Broker document format *) |
23799 | 205 |
"litcomment", |
206 |
"showcode", |
|
207 |
"setformat"] |
|
21637 | 208 |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
209 |
(* non-document/empty text, must be ignored *) |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
210 |
val doc_markup_elements_ignored = |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21637
diff
changeset
|
211 |
[ "metainfo", "openblock", "closeblock", |
23799 | 212 |
"litcomment", "showcode", "setformat" ] |
213 |
||
214 |
end; |