author | aspinall |
Sun, 17 Dec 2006 22:43:50 +0100 | |
changeset 21867 | 8750fbc28d5c |
parent 21858 | 05f57309170c |
child 21902 | 8e5e2571c716 |
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 *) |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
108 |
|
21637 | 109 |
fun cleardisplay vs = |
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 |
||
116 |
fun normalresponse vs = |
|
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 |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
129 |
|
21637 | 130 |
fun errorresponse vs = |
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 |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
143 |
|
21637 | 144 |
|
145 |
fun informfile lr vs = |
|
146 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
147 |
val url = #url vs |
21637 | 148 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
149 |
XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, []) |
21637 | 150 |
end |
151 |
||
152 |
val informfileloaded = informfile "loaded" |
|
153 |
val informfileretracted = informfile "retracted" |
|
154 |
||
155 |
fun proofstate vs = |
|
156 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
157 |
val pgml = #pgml vs |
21637 | 158 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
159 |
XML.Elem("proofstate", [], pgml) |
21637 | 160 |
end |
161 |
||
162 |
fun metainforesponse vs = |
|
163 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
164 |
val attrs = #attrs vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
165 |
val content = #content vs |
21637 | 166 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
167 |
XML.Elem ("metainforesponse", attrs, content) |
21637 | 168 |
end |
169 |
||
170 |
fun lexicalstructure vs = |
|
171 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
172 |
val content = #content vs |
21637 | 173 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
174 |
XML.Elem ("lexicalstructure", [], content) |
21637 | 175 |
end |
176 |
||
177 |
fun proverinfo vs = |
|
178 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
179 |
val name = #name vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
180 |
val version = #version vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
181 |
val instance = #instance vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
182 |
val descr = #descr vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
183 |
val url = #url vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
184 |
val filenameextns = #filenameextns vs |
21637 | 185 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
186 |
XML.Elem ("proverinfo", |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
187 |
[("name", name), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
188 |
("version", version), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
189 |
("instance", instance), |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
190 |
("descr", descr), |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21655
diff
changeset
|
191 |
("url", Url.implode url), |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
192 |
("filenameextns", filenameextns)], |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
193 |
[]) |
21637 | 194 |
end |
195 |
||
196 |
fun setids vs = |
|
197 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
198 |
val idtables = #idtables vs |
21637 | 199 |
in |
21867 | 200 |
XML.Elem ("setids",[],map idtable_to_xml idtables) |
21637 | 201 |
end |
202 |
||
203 |
fun addids vs = |
|
204 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
205 |
val idtables = #idtables vs |
21637 | 206 |
in |
21867 | 207 |
XML.Elem ("addids",[],map idtable_to_xml idtables) |
21637 | 208 |
end |
209 |
||
210 |
fun delids vs = |
|
211 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
212 |
val idtables = #idtables vs |
21637 | 213 |
in |
21867 | 214 |
XML.Elem ("delids",[],map idtable_to_xml idtables) |
21637 | 215 |
end |
216 |
||
217 |
||
218 |
fun acceptedpgipelems vs = |
|
219 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
220 |
val pgipelems = #pgipelems vs |
21651 | 221 |
fun async_attrs b = if b then attr "async" "true" else [] |
222 |
fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs) |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
223 |
fun singlepgipelem (e,async,attrs) = |
21655
01b2d13153c8
Document structure in pgip_markup.ML. Minor fixes.
aspinall
parents:
21651
diff
changeset
|
224 |
XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e]) |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
225 |
|
21637 | 226 |
in |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
227 |
XML.Elem ("acceptedpgipelems", [], |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
228 |
map singlepgipelem pgipelems) |
21637 | 229 |
end |
230 |
||
231 |
||
232 |
fun hasprefs vs = |
|
233 |
let |
|
234 |
val prefcategory = #prefcategory vs |
|
235 |
val prefs = #prefs vs |
|
236 |
in |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
237 |
XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs) |
21637 | 238 |
end |
239 |
||
240 |
fun prefval vs = |
|
241 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
242 |
val name = #name vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
243 |
val value = #value vs |
21637 | 244 |
in |
21651 | 245 |
XML.Elem("prefval", attr "name" name, [XML.Text value]) |
21637 | 246 |
end |
247 |
||
248 |
fun idvalue vs = |
|
249 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
250 |
val name = #name vs |
21867 | 251 |
val objtype_attrs = attrs_of_objtype (#objtype vs) |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
252 |
val text = #text vs |
21637 | 253 |
in |
21867 | 254 |
XML.Elem("idvalue", attr "name" name @ objtype_attrs, text) |
21637 | 255 |
end |
256 |
||
257 |
||
258 |
fun informguise vs = |
|
259 |
let |
|
260 |
val file = #file vs |
|
261 |
val theory = #theory vs |
|
262 |
val theorem = #theorem vs |
|
263 |
val proofpos = #proofpos vs |
|
264 |
||
265 |
fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])] |
|
266 |
||
267 |
val guisefile = elto "guisefile" attrs_of_pgipurl file |
|
268 |
val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory |
|
269 |
val guiseproof = elto "guiseproof" |
|
21651 | 270 |
(fn thm=>(attr "thmname" thm) @ |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
271 |
(opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem |
21637 | 272 |
in |
273 |
XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof) |
|
274 |
end |
|
275 |
||
276 |
fun parseresult vs = |
|
277 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
278 |
val attrs = #attrs vs |
21867 | 279 |
val doc = #doc vs |
280 |
val errs = #errs vs |
|
281 |
val xmldoc = PgipMarkup.output_doc doc |
|
21637 | 282 |
in |
21867 | 283 |
XML.Elem("parseresult", attrs, errs@xmldoc) |
21637 | 284 |
end |
285 |
||
286 |
fun usespgip vs = |
|
287 |
let |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
288 |
val version = #version vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
289 |
val acceptedelems = acceptedpgipelems vs |
21637 | 290 |
in |
21651 | 291 |
XML.Elem("usespgip", attr "version" version, [acceptedelems]) |
21637 | 292 |
end |
293 |
||
294 |
fun usespgml vs = |
|
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 |
||
301 |
fun pgip vs = |
|
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 |
||
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
323 |
fun ready vs = XML.Elem("ready",[],[]) |
21637 | 324 |
|
325 |
||
326 |
fun output pgipoutput = case pgipoutput of |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
327 |
Cleardisplay vs => cleardisplay vs |
21637 | 328 |
| Normalresponse vs => normalresponse vs |
329 |
| Errorresponse vs => errorresponse vs |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
330 |
| Informfileloaded vs => informfileloaded vs |
21637 | 331 |
| Informfileretracted vs => informfileretracted vs |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
332 |
| Proofstate vs => proofstate vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
333 |
| Metainforesponse vs => metainforesponse vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
334 |
| Lexicalstructure vs => lexicalstructure vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
335 |
| Proverinfo vs => proverinfo vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
336 |
| Setids vs => setids vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
337 |
| Addids vs => addids vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
338 |
| Delids vs => delids vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
339 |
| Hasprefs vs => hasprefs vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
340 |
| Prefval vs => prefval vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
341 |
| Idvalue vs => idvalue vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
342 |
| Informguise vs => informguise vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
343 |
| Parseresult vs => parseresult vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
344 |
| Usespgip vs => usespgip vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
345 |
| Usespgml vs => usespgml vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
346 |
| Pgip vs => pgip vs |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset
|
347 |
| Ready vs => ready vs |
21637 | 348 |
|
349 |
end |
|
350 |