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