author | aspinall |
Fri, 29 Dec 2006 16:46:39 +0100 | |
changeset 21929 | fb0cd849bc60 |
parent 21902 | 8e5e2571c716 |
child 21940 | fbd068dd4d29 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/pgip_output.ML |
2 |
ID: $Id$ |
|
3 |
Author: David Aspinall |
|
4 |
||
5 |
PGIP abstraction: output commands |
|
6 |
*) |
|
7 |
||
8 |
signature PGIPOUTPUT = |
|
9 |
sig |
|
10 |
(* These are the PGIP messages which the prover emits. *) |
|
11 |
datatype pgipoutput = |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
12 |
Cleardisplay of { area: PgipTypes.displayarea } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
13 |
| Normalresponse of { area: PgipTypes.displayarea, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
14 |
urgent: bool, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
15 |
messagecategory: PgipTypes.messagecategory, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
16 |
content: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
17 |
| Errorresponse of { fatality: PgipTypes.fatality, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
18 |
area: PgipTypes.displayarea option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
19 |
location: PgipTypes.location option, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
20 |
content: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
21 |
| Informfileloaded of { url: PgipTypes.pgipurl } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
22 |
| Informfileretracted of { url: PgipTypes.pgipurl } |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
23 |
| Proofstate of { pgml: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
24 |
| Metainforesponse of { attrs: XML.attributes, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
25 |
content: XML.content } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
26 |
| Lexicalstructure of { content: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
27 |
| Proverinfo of { name: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
28 |
version: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
29 |
instance: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
30 |
descr: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
31 |
url: Url.T, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
32 |
filenameextns: string } |
21867 | 33 |
| Setids of { idtables: PgipTypes.idtable list } |
34 |
| Delids of { idtables: PgipTypes.idtable list } |
|
35 |
| Addids of { idtables: PgipTypes.idtable list } |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
36 |
| Hasprefs of { prefcategory: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
37 |
prefs: PgipTypes.preference list } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
38 |
| Prefval of { name: string, value: string } |
21867 | 39 |
| Idvalue of { name: PgipTypes.objname, |
40 |
objtype: PgipTypes.objtype, |
|
41 |
text: XML.content } |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
42 |
| Informguise of { file : PgipTypes.pgipurl option, |
21867 | 43 |
theory: PgipTypes.objname option, |
44 |
theorem: PgipTypes.objname option, |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
45 |
proofpos: int option } |
21867 | 46 |
| Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, |
47 |
errs: XML.content } (* errs to become PGML *) |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
48 |
| Usespgip of { version: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
49 |
pgipelems: (string * bool * string list) list } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
50 |
| Usespgml of { version: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
51 |
| Pgip of { tag: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
52 |
class: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
53 |
seq: int, id: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
54 |
destid: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
55 |
refid: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
56 |
refseq: int option, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
57 |
content: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
58 |
| Ready of { } |
21637 | 59 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
60 |
val output : pgipoutput -> XML.tree |
21637 | 61 |
end |
62 |
||
63 |
structure PgipOutput : PGIPOUTPUT = |
|
64 |
struct |
|
65 |
open PgipTypes |
|
66 |
||
67 |
datatype pgipoutput = |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
68 |
Cleardisplay of { area: displayarea } |
21637 | 69 |
| Normalresponse of { area: displayarea, urgent: bool, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
70 |
messagecategory: messagecategory, content: XML.content } |
21637 | 71 |
| Errorresponse of { area: displayarea option, fatality: fatality, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
72 |
location: location option, content: XML.content } |
21637 | 73 |
| Informfileloaded of { url: Path.T } |
74 |
| Informfileretracted of { url: Path.T } |
|
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
75 |
| Proofstate of { pgml: XML.content } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
76 |
| Metainforesponse of { attrs: XML.attributes, content: XML.content } |
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
77 |
| Lexicalstructure of { content: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
78 |
| Proverinfo of { name: string, version: string, instance: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
79 |
descr: string, url: Url.T, filenameextns: string } |
21867 | 80 |
| Setids of { idtables: PgipTypes.idtable list } |
81 |
| Delids of { idtables: PgipTypes.idtable list } |
|
82 |
| Addids of { idtables: PgipTypes.idtable list } |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
83 |
| Hasprefs of { prefcategory: string option, prefs: preference list } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
84 |
| Prefval of { name: string, value: string } |
21867 | 85 |
| Idvalue of { name: PgipTypes.objname, |
86 |
objtype: PgipTypes.objtype, |
|
87 |
text: XML.content } |
|
88 |
| Informguise of { file : PgipTypes.pgipurl option, |
|
89 |
theory: PgipTypes.objname option, |
|
90 |
theorem: PgipTypes.objname option, |
|
91 |
proofpos: int option } |
|
92 |
| Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument, |
|
93 |
errs: XML.content } (* errs to become PGML *) |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
94 |
| Usespgip of { version: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
95 |
pgipelems: (string * bool * string list) list } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
96 |
| Usespgml of { version: string } |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
97 |
| Pgip of { tag: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
98 |
class: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
99 |
seq: int, id: string, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
100 |
destid: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
101 |
refid: string option, |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
102 |
refseq: int option, |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
103 |
content: XML.content } |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
104 |
| Ready of { } |
21637 | 105 |
|
106 |
||
107 |
(* Construct output XML messages *) |
|
21902 | 108 |
|
109 |
fun cleardisplay (Cleardisplay vs) = |
|
21637 | 110 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
111 |
val area = #area vs |
21637 | 112 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
113 |
XML.Elem ("cleardisplay", (attrs_of_displayarea area), []) |
21637 | 114 |
end |
115 |
||
21902 | 116 |
fun normalresponse (Normalresponse vs) = |
21637 | 117 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
118 |
val area = #area vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
119 |
val urgent = #urgent vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
120 |
val messagecategory = #messagecategory vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
121 |
val content = #content vs |
21637 | 122 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
123 |
XML.Elem ("normalresponse", |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
124 |
(attrs_of_displayarea area) @ |
21651 | 125 |
(if urgent then attr "urgent" "true" else []) @ |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
126 |
(attrs_of_messagecategory messagecategory), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
127 |
content) |
21637 | 128 |
end |
21902 | 129 |
|
130 |
fun errorresponse (Errorresponse vs) = |
|
21637 | 131 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
132 |
val area = #area vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
133 |
val fatality = #fatality vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
134 |
val location = #location vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
135 |
val content = #content vs |
21637 | 136 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
137 |
XML.Elem ("errorresponse", |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
138 |
(the_default [] (Option.map attrs_of_displayarea area)) @ |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
139 |
(attrs_of_fatality fatality) @ |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
140 |
(the_default [] (Option.map attrs_of_location location)), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
141 |
content) |
21637 | 142 |
end |
143 |
||
21902 | 144 |
fun informfileloaded (Informfileloaded vs) = |
21637 | 145 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
146 |
val url = #url vs |
21637 | 147 |
in |
21902 | 148 |
XML.Elem ("informfileloaded", attrs_of_pgipurl url, []) |
21637 | 149 |
end |
150 |
||
21902 | 151 |
fun informfileretracted (Informfileretracted vs) = |
152 |
let |
|
153 |
val url = #url vs |
|
154 |
in |
|
155 |
XML.Elem ("informfileretracted", attrs_of_pgipurl url, []) |
|
156 |
end |
|
21637 | 157 |
|
21902 | 158 |
fun proofstate (Proofstate vs) = |
21637 | 159 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
160 |
val pgml = #pgml vs |
21637 | 161 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
162 |
XML.Elem("proofstate", [], pgml) |
21637 | 163 |
end |
164 |
||
21902 | 165 |
fun metainforesponse (Metainforesponse vs) = |
21637 | 166 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
167 |
val attrs = #attrs vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
168 |
val content = #content vs |
21637 | 169 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
170 |
XML.Elem ("metainforesponse", attrs, content) |
21637 | 171 |
end |
172 |
||
21902 | 173 |
fun lexicalstructure (Lexicalstructure vs) = |
21637 | 174 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
175 |
val content = #content vs |
21637 | 176 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
177 |
XML.Elem ("lexicalstructure", [], content) |
21637 | 178 |
end |
179 |
||
21902 | 180 |
fun proverinfo (Proverinfo vs) = |
21637 | 181 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
182 |
val name = #name vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
183 |
val version = #version vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
184 |
val instance = #instance vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
185 |
val descr = #descr vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
186 |
val url = #url vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
187 |
val filenameextns = #filenameextns vs |
21637 | 188 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
189 |
XML.Elem ("proverinfo", |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
190 |
[("name", name), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
191 |
("version", version), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
192 |
("instance", instance), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
193 |
("descr", descr), |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21655
diff
changeset
|
194 |
("url", Url.implode url), |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
195 |
("filenameextns", filenameextns)], |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
196 |
[]) |
21637 | 197 |
end |
198 |
||
21902 | 199 |
fun setids (Setids vs) = |
21637 | 200 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
201 |
val idtables = #idtables vs |
21637 | 202 |
in |
21867 | 203 |
XML.Elem ("setids",[],map idtable_to_xml idtables) |
21637 | 204 |
end |
205 |
||
21902 | 206 |
fun addids (Addids vs) = |
21637 | 207 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
208 |
val idtables = #idtables vs |
21637 | 209 |
in |
21867 | 210 |
XML.Elem ("addids",[],map idtable_to_xml idtables) |
21637 | 211 |
end |
212 |
||
21902 | 213 |
fun delids (Delids vs) = |
21637 | 214 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
215 |
val idtables = #idtables vs |
21637 | 216 |
in |
21867 | 217 |
XML.Elem ("delids",[],map idtable_to_xml idtables) |
21637 | 218 |
end |
219 |
||
21902 | 220 |
fun hasprefs (Hasprefs vs) = |
21637 | 221 |
let |
222 |
val prefcategory = #prefcategory vs |
|
223 |
val prefs = #prefs vs |
|
224 |
in |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
225 |
XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs) |
21637 | 226 |
end |
227 |
||
21902 | 228 |
fun prefval (Prefval vs) = |
21637 | 229 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
230 |
val name = #name vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
231 |
val value = #value vs |
21637 | 232 |
in |
21651 | 233 |
XML.Elem("prefval", attr "name" name, [XML.Text value]) |
21637 | 234 |
end |
235 |
||
21902 | 236 |
fun idvalue (Idvalue vs) = |
21637 | 237 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
238 |
val name = #name vs |
21867 | 239 |
val objtype_attrs = attrs_of_objtype (#objtype vs) |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
240 |
val text = #text vs |
21637 | 241 |
in |
21867 | 242 |
XML.Elem("idvalue", attr "name" name @ objtype_attrs, text) |
21902 | 243 |
end |
21637 | 244 |
|
21902 | 245 |
fun informguise (Informguise vs) = |
21637 | 246 |
let |
247 |
val file = #file vs |
|
248 |
val theory = #theory vs |
|
249 |
val theorem = #theorem vs |
|
250 |
val proofpos = #proofpos vs |
|
251 |
||
252 |
fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])] |
|
253 |
||
254 |
val guisefile = elto "guisefile" attrs_of_pgipurl file |
|
255 |
val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory |
|
256 |
val guiseproof = elto "guiseproof" |
|
21651 | 257 |
(fn thm=>(attr "thmname" thm) @ |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
258 |
(opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem |
21637 | 259 |
in |
260 |
XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof) |
|
261 |
end |
|
262 |
||
21902 | 263 |
fun parseresult (Parseresult vs) = |
21637 | 264 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
265 |
val attrs = #attrs vs |
21867 | 266 |
val doc = #doc vs |
267 |
val errs = #errs vs |
|
268 |
val xmldoc = PgipMarkup.output_doc doc |
|
21637 | 269 |
in |
21867 | 270 |
XML.Elem("parseresult", attrs, errs@xmldoc) |
21637 | 271 |
end |
272 |
||
21902 | 273 |
fun acceptedpgipelems (Usespgip vs) = |
274 |
let |
|
275 |
val pgipelems = #pgipelems vs |
|
276 |
fun async_attrs b = if b then attr "async" "true" else [] |
|
277 |
fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs) |
|
278 |
fun singlepgipelem (e,async,attrs) = |
|
279 |
XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e]) |
|
280 |
||
281 |
in |
|
282 |
XML.Elem ("acceptedpgipelems", [], |
|
283 |
map singlepgipelem pgipelems) |
|
284 |
end |
|
285 |
||
286 |
fun usespgip (Usespgip vs) = |
|
21637 | 287 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
288 |
val version = #version vs |
21902 | 289 |
val acceptedelems = acceptedpgipelems (Usespgip vs) |
21637 | 290 |
in |
21651 | 291 |
XML.Elem("usespgip", attr "version" version, [acceptedelems]) |
21637 | 292 |
end |
293 |
||
21902 | 294 |
fun usespgml (Usespgml vs) = |
21637 | 295 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
296 |
val version = #version vs |
21637 | 297 |
in |
21651 | 298 |
XML.Elem("usespgml", attr "version" version, []) |
21637 | 299 |
end |
300 |
||
21902 | 301 |
fun pgip (Pgip vs) = |
21637 | 302 |
let |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
303 |
val tag = #tag vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
304 |
val class = #class vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
305 |
val seq = #seq vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
306 |
val id = #id vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
307 |
val destid = #destid vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
308 |
val refid = #refid vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
309 |
val refseq = #refseq vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
310 |
val content = #content vs |
21637 | 311 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
312 |
XML.Elem("pgip", |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
313 |
opt_attr "tag" tag @ |
21651 | 314 |
attr "id" id @ |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
315 |
opt_attr "destid" destid @ |
21651 | 316 |
attr "class" class @ |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
317 |
opt_attr "refid" refid @ |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
318 |
opt_attr_map string_of_int "refseq" refseq @ |
21651 | 319 |
attr "seq" (string_of_int seq), |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
320 |
content) |
21637 | 321 |
end |
322 |
||
21902 | 323 |
fun ready (Ready vs) = XML.Elem("ready",[],[]) |
21637 | 324 |
|
325 |
||
326 |
fun output pgipoutput = case pgipoutput of |
|
21929 | 327 |
Cleardisplay _ => cleardisplay pgipoutput |
21902 | 328 |
| Normalresponse _ => normalresponse pgipoutput |
329 |
| Errorresponse _ => errorresponse pgipoutput |
|
330 |
| Informfileloaded _ => informfileloaded pgipoutput |
|
331 |
| Informfileretracted _ => informfileretracted pgipoutput |
|
332 |
| Proofstate _ => proofstate pgipoutput |
|
333 |
| Metainforesponse _ => metainforesponse pgipoutput |
|
334 |
| Lexicalstructure _ => lexicalstructure pgipoutput |
|
335 |
| Proverinfo _ => proverinfo pgipoutput |
|
336 |
| Setids _ => setids pgipoutput |
|
337 |
| Addids _ => addids pgipoutput |
|
338 |
| Delids _ => delids pgipoutput |
|
339 |
| Hasprefs _ => hasprefs pgipoutput |
|
340 |
| Prefval _ => prefval pgipoutput |
|
341 |
| Idvalue _ => idvalue pgipoutput |
|
342 |
| Informguise _ => informguise pgipoutput |
|
343 |
| Parseresult _ => parseresult pgipoutput |
|
344 |
| Usespgip _ => usespgip pgipoutput |
|
345 |
| Usespgml _ => usespgml pgipoutput |
|
346 |
| Pgip _ => pgip pgipoutput |
|
347 |
| Ready _ => ready pgipoutput |
|
21637 | 348 |
|
349 |
end |
|
350 |