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