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