author | aspinall |
Sat, 17 Feb 2007 18:00:59 +0100 | |
changeset 22337 | d4599c206446 |
parent 22249 | 5460a5e4caa2 |
child 22397 | ec7ecf706955 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/proof_general_pgip.ML |
2 |
ID: $Id$ |
|
3 |
Author: David Aspinall and Markus Wenzel |
|
4 |
||
5 |
Isabelle configuration for Proof General using PGIP protocol. |
|
21940 | 6 |
See http://proofgeneral.inf.ed.ac.uk/kit |
21637 | 7 |
*) |
8 |
||
9 |
signature PROOF_GENERAL_PGIP = |
|
10 |
sig |
|
21940 | 11 |
val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *) |
21642 | 12 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
13 |
(* These two are just to support the semi-PGIP Emacs mode *) |
21940 | 14 |
val init_pgip_channel: (string -> unit) -> unit |
15 |
val process_pgip: string -> unit |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
16 |
|
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
17 |
(* Yet more message functions... *) |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
18 |
val nonfatal_error : string -> unit (* recoverable error *) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
19 |
val log_msg : string -> unit (* for internal log messages *) |
22163 | 20 |
val error_with_pos : PgipTypes.fatality -> Position.T -> string -> unit |
22159 | 21 |
|
22163 | 22 |
val get_currently_open_file : unit -> Path.T option (* interface focus *) |
21637 | 23 |
end |
24 |
||
25 |
structure ProofGeneralPgip : PROOF_GENERAL_PGIP = |
|
26 |
struct |
|
27 |
||
28 |
open Pgip; |
|
29 |
||
21949 | 30 |
|
21637 | 31 |
(* print modes *) |
32 |
||
33 |
val proof_generalN = "ProofGeneral"; (*token markup (colouring vars, etc.)*) |
|
34 |
val pgmlN = "PGML"; (*XML escapes and PGML symbol elements*) |
|
35 |
val thm_depsN = "thm_deps"; (*meta-information about theorem deps*) |
|
36 |
||
37 |
||
38 |
(* text output: print modes for xsymbol and PGML *) |
|
39 |
||
40 |
local |
|
41 |
||
42 |
fun xsym_output "\\" = "\\\\" |
|
43 |
| xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; |
|
44 |
||
45 |
fun xsymbols_output s = |
|
21940 | 46 |
if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then |
21637 | 47 |
let val syms = Symbol.explode s |
48 |
in (implode (map xsym_output syms), real (Symbol.length syms)) end |
|
49 |
else Symbol.default_output s; |
|
50 |
||
51 |
(* XML immediately rendered pretty printer. Take care not to double escape *) |
|
52 |
fun pgml_sym s = |
|
53 |
(case Symbol.decode s of |
|
54 |
Symbol.Char s => XML.text s |
|
21940 | 55 |
| Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s] |
21637 | 56 |
| Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *) |
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
57 |
| Symbol.Raw s => Symbol.decode_raw s); |
21637 | 58 |
|
59 |
fun pgml_output str = |
|
60 |
let val syms = Symbol.explode str |
|
61 |
in (implode (map pgml_sym syms), real (Symbol.length syms)) end; |
|
62 |
||
63 |
in |
|
64 |
||
65 |
fun setup_xsymbols_output () = |
|
21940 | 66 |
Output.add_mode Symbol.xsymbolsN |
21637 | 67 |
(xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw); |
68 |
||
69 |
fun setup_pgml_output () = |
|
70 |
Output.add_mode pgmlN |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
71 |
(pgml_output, K pgml_output, Symbol.default_indent, I); (* Symbol.encode_raw); *) |
21637 | 72 |
|
73 |
end; |
|
74 |
||
75 |
||
76 |
(* token translations *) |
|
77 |
||
78 |
local |
|
79 |
||
80 |
val class_tag = "class" |
|
81 |
val tfree_tag = "tfree" |
|
82 |
val tvar_tag = "tvar" |
|
83 |
val free_tag = "free" |
|
84 |
val bound_tag = "bound" |
|
85 |
val var_tag = "var" |
|
86 |
val skolem_tag = "skolem" |
|
87 |
||
88 |
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; |
|
89 |
||
21940 | 90 |
fun tagit kind x = |
21949 | 91 |
(xml_atom kind x, real (Symbol.length (Symbol.explode x))); |
21637 | 92 |
|
93 |
fun free_or_skolem x = |
|
94 |
(case try Name.dest_skolem x of |
|
95 |
NONE => tagit free_tag x |
|
96 |
| SOME x' => tagit skolem_tag x'); |
|
97 |
||
98 |
fun var_or_skolem s = |
|
99 |
(case Syntax.read_variable s of |
|
100 |
SOME (x, i) => |
|
101 |
(case try Name.dest_skolem x of |
|
102 |
NONE => tagit var_tag s |
|
103 |
| SOME x' => tagit skolem_tag |
|
104 |
(setmp show_question_marks true Syntax.string_of_vname (x', i))) |
|
105 |
| NONE => tagit var_tag s); |
|
106 |
||
107 |
val proof_general_trans = |
|
108 |
Syntax.tokentrans_mode proof_generalN |
|
109 |
[("class", tagit class_tag), |
|
110 |
("tfree", tagit tfree_tag), |
|
111 |
("tvar", tagit tvar_tag), |
|
112 |
("free", free_or_skolem), |
|
113 |
("bound", tagit bound_tag), |
|
114 |
("var", var_or_skolem)]; |
|
115 |
||
116 |
in |
|
117 |
||
118 |
val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans); |
|
119 |
||
120 |
end; |
|
121 |
||
122 |
||
123 |
(** assembling and issuing PGIP packets **) |
|
124 |
||
125 |
val pgip_refid = ref NONE: string option ref; |
|
126 |
val pgip_refseq = ref NONE: int option ref; |
|
127 |
||
128 |
local |
|
129 |
val pgip_class = "pg" |
|
130 |
val pgip_tag = "Isabelle/Isar" |
|
131 |
val pgip_id = ref "" |
|
132 |
val pgip_seq = ref 0 |
|
133 |
fun pgip_serial () = inc pgip_seq |
|
134 |
||
135 |
fun assemble_pgips pgips = |
|
21940 | 136 |
Pgip { tag = SOME pgip_tag, |
137 |
class = pgip_class, |
|
138 |
seq = pgip_serial(), |
|
139 |
id = !pgip_id, |
|
140 |
destid = !pgip_refid, |
|
141 |
(* destid=refid since Isabelle only communicates back to sender *) |
|
142 |
refid = !pgip_refid, |
|
143 |
refseq = !pgip_refseq, |
|
144 |
content = pgips } |
|
21637 | 145 |
in |
146 |
||
147 |
fun init_pgip_session_id () = |
|
148 |
pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ |
|
149 |
getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) |
|
150 |
||
151 |
fun matching_pgip_id id = (id = !pgip_id) |
|
152 |
||
21940 | 153 |
val output_xml_fn = ref writeln_default |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
154 |
fun output_xml s = (!output_xml_fn) (XML.string_of_tree s); (* TODO: string buffer *) |
21637 | 155 |
|
21940 | 156 |
fun issue_pgip_rawtext str = |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
157 |
output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str])) |
21637 | 158 |
|
159 |
fun issue_pgips pgipops = |
|
160 |
output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops))); |
|
161 |
||
162 |
fun issue_pgip pgipop = |
|
163 |
output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop])); |
|
164 |
||
165 |
end; |
|
166 |
||
167 |
||
168 |
(** messages and notification **) |
|
169 |
||
170 |
local |
|
171 |
val delay_msgs = ref false (*true: accumulate messages*) |
|
172 |
val delayed_msgs = ref [] |
|
173 |
||
174 |
fun queue_or_issue pgip = |
|
21940 | 175 |
if ! delay_msgs then |
176 |
delayed_msgs := pgip :: ! delayed_msgs |
|
177 |
else issue_pgip pgip |
|
21637 | 178 |
in |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
179 |
(* Normal responses are messages for the user *) |
21940 | 180 |
fun normalmsg area cat urgent s = |
181 |
let |
|
182 |
val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) |
|
183 |
val pgip = Normalresponse {area=area,messagecategory=cat, |
|
184 |
urgent=urgent,content=[content] } |
|
185 |
in |
|
186 |
queue_or_issue pgip |
|
187 |
end |
|
21637 | 188 |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
189 |
(* Error responses are error messages for the user, or system-level messages *) |
21885
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
190 |
fun errormsg fatality s = |
21940 | 191 |
let |
21885
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
192 |
val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) |
21940 | 193 |
val pgip = Errorresponse {area=NONE,fatality=fatality, |
194 |
content=[content], |
|
195 |
location=NONE} |
|
196 |
in |
|
197 |
queue_or_issue pgip |
|
198 |
end |
|
21637 | 199 |
|
22159 | 200 |
(* Error responses with useful locations *) |
201 |
fun error_with_pos fatality pos s = |
|
202 |
let |
|
203 |
val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) |
|
204 |
val pgip = Errorresponse {area=NONE,fatality=fatality, |
|
205 |
content=[content], |
|
206 |
location=SOME (PgipIsabelle.location_of_position pos)} |
|
207 |
in |
|
208 |
queue_or_issue pgip |
|
209 |
end |
|
210 |
||
21637 | 211 |
fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []) |
212 |
fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs) |
|
213 |
end; |
|
214 |
||
215 |
(* NB: all of the standard error/message functions now expect already-escaped text. |
|
216 |
FIXME: this may cause us problems now we're generating trees; on the other |
|
21940 | 217 |
hand the output functions were tuned some time ago, so it ought to be |
21637 | 218 |
enough to use Rawtext always above. *) |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
219 |
(* NB 2: all of standard functions print strings terminated with new lines, but we don't |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
220 |
add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
221 |
can't be written without newlines. *) |
21637 | 222 |
|
223 |
fun setup_messages () = |
|
21885
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
224 |
(writeln_fn := (fn s => normalmsg Message Normal false s); |
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
225 |
priority_fn := (fn s => normalmsg Message Normal true s); |
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
226 |
tracing_fn := (fn s => normalmsg Message Tracing false s); |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
227 |
info_fn := (fn s => errormsg Info s); |
22001 | 228 |
warning_fn := (fn s => errormsg Warning s); |
22014
4b70cbd96007
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
wenzelm
parents:
22001
diff
changeset
|
229 |
error_fn := (fn s => errormsg Fatal s); |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
230 |
panic_fn := (fn s => errormsg Panic s); |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
231 |
debug_fn := (fn s => errormsg Debug s)); |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
232 |
|
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
233 |
fun nonfatal_error s = errormsg Nonfatal s; |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
234 |
fun log_msg s = errormsg Log s; |
21983
9fb029d1189b
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
aspinall
parents:
21972
diff
changeset
|
235 |
|
21637 | 236 |
|
237 |
(* immediate messages *) |
|
238 |
||
239 |
fun tell_clear_goals () = issue_pgip (Cleardisplay {area=Display}) |
|
240 |
fun tell_clear_response () = issue_pgip (Cleardisplay {area=Message}) |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
241 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
242 |
fun tell_file_loaded completed path = |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
243 |
issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path, |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
244 |
completed=completed}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
245 |
fun tell_file_outdated completed path = |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
246 |
issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path, |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
247 |
completed=completed}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
248 |
fun tell_file_retracted completed path = |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
249 |
issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path, |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
250 |
completed=completed}) |
21637 | 251 |
|
252 |
||
253 |
||
254 |
(** theory / proof state output **) |
|
255 |
||
256 |
local |
|
257 |
||
258 |
fun statedisplay prts = |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
259 |
let |
21940 | 260 |
val display = Pretty.output (Pretty.chunks prts) |
22028 | 261 |
(* TODO: add extra PGML markup for allow proof state navigation *) |
21940 | 262 |
val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display]) |
21637 | 263 |
in |
21940 | 264 |
issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]}) |
21637 | 265 |
end |
266 |
||
267 |
fun print_current_goals n m st = |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
268 |
case (Display.pretty_current_goals n m st) of |
22028 | 269 |
[] => tell_clear_goals() |
270 |
| prts => statedisplay prts |
|
21637 | 271 |
|
272 |
fun print_state b st = |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
273 |
case (Toplevel.pretty_state b st) of |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
274 |
[] => tell_clear_goals() |
22028 | 275 |
| prts => statedisplay prts |
21637 | 276 |
|
277 |
in |
|
278 |
||
279 |
fun setup_state () = |
|
280 |
(Display.print_current_goals_fn := print_current_goals; |
|
281 |
Toplevel.print_state_fn := print_state); |
|
282 |
||
283 |
end; |
|
284 |
||
285 |
||
286 |
(* theory loader actions *) |
|
287 |
||
288 |
local |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
289 |
(* da: TODO: PGIP has a completed flag so the prover can indicate to the |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
290 |
interface which files are busy performing a particular action. |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
291 |
To make use of this we need to adjust the hook in thy_info.ML |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
292 |
(may actually be difficult to tell the interface *which* action is in |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
293 |
progress, but we could add a generic "Lock" action which uses |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
294 |
informfileloaded: the broker/UI should not infer too much from incomplete |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
295 |
operations). |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
296 |
*) |
21637 | 297 |
fun trace_action action name = |
298 |
if action = ThyInfo.Update then |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
299 |
List.app (tell_file_loaded true) (ThyInfo.loaded_files name) |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
300 |
else if action = ThyInfo.Outdate then |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
301 |
List.app (tell_file_outdated true) (ThyInfo.loaded_files name) |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
302 |
else if action = ThyInfo.Remove then |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
303 |
List.app (tell_file_retracted true) (ThyInfo.loaded_files name) |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
304 |
else () |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
305 |
|
21637 | 306 |
|
307 |
in |
|
308 |
fun setup_thy_loader () = ThyInfo.add_hook trace_action; |
|
309 |
fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ()); |
|
310 |
end; |
|
311 |
||
312 |
||
21949 | 313 |
(* get informed about files *) |
21637 | 314 |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
315 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base; |
21637 | 316 |
|
317 |
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; |
|
318 |
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name; |
|
319 |
||
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
320 |
fun proper_inform_file_processed path state = |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
321 |
let val name = thy_name path in |
21637 | 322 |
if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then |
323 |
(ThyInfo.touch_child_thys name; |
|
324 |
ThyInfo.pretend_use_thy_only name handle ERROR msg => |
|
325 |
(warning msg; warning ("Failed to register theory: " ^ quote name); |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
326 |
tell_file_retracted true (Path.base path))) |
21637 | 327 |
else raise Toplevel.UNDEF |
328 |
end; |
|
329 |
||
330 |
||
331 |
(* restart top-level loop (keeps most state information) *) |
|
332 |
||
333 |
val welcome = priority o Session.welcome; |
|
334 |
||
335 |
fun restart () = |
|
336 |
(sync_thy_loader (); |
|
337 |
tell_clear_goals (); |
|
338 |
tell_clear_response (); |
|
339 |
welcome (); |
|
340 |
raise Toplevel.RESTART) |
|
341 |
||
342 |
||
343 |
(* theorem dependency output *) |
|
344 |
local |
|
345 |
||
346 |
val spaces_quote = space_implode " " o map quote; |
|
347 |
||
348 |
fun thm_deps_message (thms, deps) = |
|
21940 | 349 |
let |
350 |
val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms]) |
|
351 |
val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps]) |
|
21637 | 352 |
in |
21940 | 353 |
issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")], |
354 |
content=[valuethms,valuedeps]}) |
|
21637 | 355 |
end |
356 |
||
21969 | 357 |
fun tell_thm_deps ths = |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
358 |
if Output.has_mode thm_depsN then |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
359 |
let |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
360 |
val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
361 |
val deps = (Symtab.keys (fold Proofterm.thms_of_proof' |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
362 |
(map Thm.proof_of ths) Symtab.empty)) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
363 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
364 |
if null names orelse null deps then () |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
365 |
else thm_deps_message (spaces_quote names, spaces_quote deps) |
22225 | 366 |
end |
367 |
else () |
|
21637 | 368 |
|
369 |
in |
|
370 |
||
371 |
fun setup_present_hook () = |
|
372 |
Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res)); |
|
373 |
||
374 |
end; |
|
375 |
||
376 |
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **) |
|
377 |
||
21940 | 378 |
fun lexicalstructure_keywords () = |
21637 | 379 |
let val commands = OuterSyntax.dest_keywords () |
21940 | 380 |
fun category_of k = if k mem commands then "major" else "minor" |
21637 | 381 |
(* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *) |
21940 | 382 |
fun keyword_elt (keyword,help,kind,_) = |
383 |
XML.Elem("keyword", [("word", keyword), ("category", category_of kind)], |
|
384 |
[XML.Elem("shorthelp", [], [XML.Text help])]) |
|
385 |
in |
|
21637 | 386 |
(* Also, note we don't call init_outer_syntax here to add interface commands, |
387 |
but they should never appear in scripts anyway so it shouldn't matter *) |
|
388 |
Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) } |
|
389 |
end |
|
390 |
||
391 |
(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically; |
|
392 |
hooks needed in outer_syntax.ML to do that. *) |
|
393 |
||
394 |
||
395 |
(* Configuration: GUI config, proverinfo messages *) |
|
396 |
||
397 |
local |
|
398 |
val isabellewww = "http://isabelle.in.tum.de/" |
|
399 |
val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml" |
|
21940 | 400 |
fun orenv v d = case getenv v of "" => d | s => s |
21637 | 401 |
fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig |
402 |
fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww |
|
403 |
in |
|
404 |
fun send_pgip_config () = |
|
405 |
let |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21655
diff
changeset
|
406 |
val path = Path.explode (config_file()) |
21940 | 407 |
val ex = File.exists path |
21637 | 408 |
|
21940 | 409 |
val wwwpage = |
410 |
(Url.explode (isabelle_www())) |
|
21969 | 411 |
handle ERROR _ => |
21940 | 412 |
(Output.panic |
413 |
("Error in URL in environment variable ISABELLE_HOMEPAGE."); |
|
414 |
Url.explode isabellewww) |
|
415 |
||
416 |
val proverinfo = |
|
21637 | 417 |
Proverinfo { name = "Isabelle", |
21940 | 418 |
version = version, |
419 |
instance = Session.name(), |
|
420 |
descr = "The Isabelle/Isar theorem prover", |
|
421 |
url = wwwpage, |
|
422 |
filenameextns = ".thy;" } |
|
21637 | 423 |
in |
21940 | 424 |
if ex then |
425 |
(issue_pgip proverinfo; |
|
426 |
issue_pgip_rawtext (File.read path); |
|
427 |
issue_pgip (lexicalstructure_keywords())) |
|
21637 | 428 |
else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found") |
429 |
end; |
|
430 |
end |
|
431 |
||
432 |
||
22216
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
433 |
(* Preferences: tweak for PGIP interfaces *) |
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
434 |
|
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
435 |
val preferences = ref Preferences.preferences; |
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
436 |
|
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
437 |
fun setup_preferences_tweak() = |
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
438 |
preferences := |
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
439 |
(* PGIP uses markup for distinguishing variable types *) |
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
440 |
(!preferences |> Preferences.set_default ("show-question-marks","false") |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
441 |
|> Preferences.remove "show-question-marks"); |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
442 |
|
21637 | 443 |
|
444 |
||
445 |
(* Sending commands to Isar *) |
|
446 |
||
447 |
fun isarcmd s = |
|
448 |
s |> OuterSyntax.scan |> OuterSyntax.read |
|
21885
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
449 |
(*|> map (Toplevel.position (Position.name "PGIP message") o #3)*) |
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
450 |
|> map #3 |
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
451 |
|> Toplevel.>>>; |
21637 | 452 |
|
21940 | 453 |
(* TODO: |
21885
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
454 |
- apply a command given a transition function, e.g. IsarCmd.undo. |
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
455 |
- fix position from path of currently open file [line numbers risk garbling though]. |
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
456 |
*) |
21637 | 457 |
|
458 |
(* load an arbitrary file (must be .thy or .ML) *) |
|
459 |
||
460 |
fun use_thy_or_ml_file file = |
|
461 |
let |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21655
diff
changeset
|
462 |
val (path,extn) = Path.split_ext (Path.explode file) |
21637 | 463 |
in |
464 |
case extn of |
|
21940 | 465 |
"" => isarcmd ("use_thy " ^ quote (Path.implode path)) |
466 |
| "thy" => isarcmd ("use_thy " ^ quote (Path.implode path)) |
|
21637 | 467 |
| "ML" => isarcmd ("use " ^ quote file) |
22028 | 468 |
| other => error ("Don't know how to read a file with extension " ^ quote other) |
21637 | 469 |
end |
470 |
||
471 |
||
21867 | 472 |
(******* PGIP actions *******) |
21637 | 473 |
|
474 |
||
21940 | 475 |
(* Responses to each of the PGIP input commands. |
21637 | 476 |
These are programmed uniformly for extensibility. *) |
477 |
||
21940 | 478 |
fun askpgip (Askpgip vs) = |
21637 | 479 |
issue_pgip |
480 |
(Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported, |
|
21940 | 481 |
pgipelems = PgipIsabelle.accepted_inputs }) |
21637 | 482 |
|
21940 | 483 |
fun askpgml (Askpgml vs) = |
21637 | 484 |
issue_pgip |
21940 | 485 |
(Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported }) |
21637 | 486 |
|
21902 | 487 |
fun askprefs (Askprefs vs) = |
21940 | 488 |
let |
489 |
fun preference_of {name, descr, default, pgiptype, get, set } = |
|
490 |
{ name = name, descr = SOME descr, default = SOME default, |
|
491 |
pgiptype = pgiptype } |
|
21637 | 492 |
in |
21940 | 493 |
List.app (fn (prefcat, prefs) => |
494 |
issue_pgip (Hasprefs {prefcategory=SOME prefcat, |
|
495 |
prefs=map preference_of prefs})) |
|
22216
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
496 |
(!preferences) |
21940 | 497 |
end |
21637 | 498 |
|
21902 | 499 |
fun askconfig (Askconfig vs) = () (* TODO: add config response *) |
21637 | 500 |
|
501 |
local |
|
21940 | 502 |
fun lookuppref pref = |
503 |
case AList.lookup (op =) |
|
504 |
(map (fn p => (#name p,p)) |
|
22216
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
505 |
(maps snd (!preferences))) pref of |
21940 | 506 |
NONE => error ("Unknown prover preference: " ^ quote pref) |
507 |
| SOME p => p |
|
21637 | 508 |
in |
21940 | 509 |
fun setpref (Setpref vs) = |
510 |
let |
|
511 |
val name = #name vs |
|
512 |
val value = #value vs |
|
513 |
val set = #set (lookuppref name) |
|
21637 | 514 |
in |
21940 | 515 |
set value |
21637 | 516 |
end |
517 |
||
21902 | 518 |
fun getpref (Getpref vs) = |
21940 | 519 |
let |
520 |
val name = #name vs |
|
521 |
val get = #get (lookuppref name) |
|
522 |
in |
|
21637 | 523 |
issue_pgip (Prefval {name=name, value=get ()}) |
524 |
end |
|
525 |
end |
|
526 |
||
527 |
fun proverinit vs = restart () |
|
528 |
||
529 |
fun proverexit vs = isarcmd "quit" |
|
530 |
||
531 |
fun startquiet vs = isarcmd "disable_pr" |
|
532 |
||
533 |
fun stopquiet vs = isarcmd "enable_pr" |
|
534 |
||
21940 | 535 |
fun pgmlsymbolson vs = |
21637 | 536 |
change print_mode (fn mode => |
21940 | 537 |
remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN]) |
21637 | 538 |
|
539 |
fun pgmlsymbolsoff vs = |
|
540 |
change print_mode (remove (op =) Symbol.xsymbolsN) |
|
541 |
||
21940 | 542 |
fun dostep (Dostep vs) = |
543 |
let |
|
544 |
val text = #text vs |
|
545 |
in |
|
546 |
isarcmd text |
|
21637 | 547 |
end |
548 |
||
21902 | 549 |
fun undostep (Undostep vs) = |
21940 | 550 |
let |
551 |
val times = #times vs |
|
552 |
in |
|
553 |
isarcmd ("undos_proof " ^ Int.toString times) |
|
21637 | 554 |
end |
555 |
||
556 |
fun redostep vs = isarcmd "redo" |
|
21940 | 557 |
|
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
558 |
fun abortgoal vs = isarcmd "kill" (* was: ProofGeneral.kill_proof *) |
21637 | 559 |
|
560 |
||
21867 | 561 |
(*** PGIP identifier tables ***) |
562 |
||
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
563 |
(* TODO: these ones should be triggered by hooks after a |
22159 | 564 |
declaration addition/removal, to be sent automatically. *) |
21867 | 565 |
|
22159 | 566 |
fun addids t = issue_pgip (Addids {idtables = [t]}) |
567 |
fun delids t = issue_pgip (Delids {idtables = [t]}) |
|
21867 | 568 |
|
21940 | 569 |
fun askids (Askids vs) = |
21637 | 570 |
let |
21940 | 571 |
val url = #url vs (* ask for identifiers within a file *) |
572 |
val thyname = #thyname vs (* ask for identifiers within a theory *) |
|
573 |
val objtype = #objtype vs (* ask for identifiers of a particular type *) |
|
21867 | 574 |
|
21940 | 575 |
fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} |
21867 | 576 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
577 |
fun setids t = issue_pgip (Setids {idtables = [t]}) |
22159 | 578 |
|
22225 | 579 |
(* fake one-level nested "subtheories" by picking apart names. *) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
580 |
val thms_of_thy = |
22243
0f24888c8591
proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);
wenzelm
parents:
22228
diff
changeset
|
581 |
map fst o NameSpace.extern_table o PureThy.theorems_of o ThyInfo.get_theory |
0f24888c8591
proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);
wenzelm
parents:
22228
diff
changeset
|
582 |
val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy |
22225 | 583 |
fun thy_prefix s = case space_explode NameSpace.separator s of |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
584 |
x::_::_ => SOME x (* String.find? *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
585 |
| _ => NONE |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
586 |
fun subthys_of_thy s = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
587 |
foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) [] |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
588 |
(map thy_prefix (thms_of_thy s)) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
589 |
fun subthms_of_thy thy = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
590 |
(case thy_prefix thy of |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
591 |
NONE => immed_thms_of_thy thy |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
592 |
| SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy)) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
593 |
(thms_of_thy prf)) |
22225 | 594 |
val qualified_thms_of_thy = (* for global query with single response *) |
22249
5460a5e4caa2
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
aspinall
parents:
22243
diff
changeset
|
595 |
(map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory; |
5460a5e4caa2
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
aspinall
parents:
22243
diff
changeset
|
596 |
(* da: this version is equivalent to my previous, but splits up theorem sets with names |
5460a5e4caa2
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
aspinall
parents:
22243
diff
changeset
|
597 |
that I can't get to access later with get_thm. Anyway, would rather use sets. |
5460a5e4caa2
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
aspinall
parents:
22243
diff
changeset
|
598 |
Is above right way to get qualified names in that case? Filtering required again? |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
599 |
map PureThy.get_name_hint o filter PureThy.has_name_hint o |
22249
5460a5e4caa2
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
aspinall
parents:
22243
diff
changeset
|
600 |
map snd o PureThy.thms_of o ThyInfo.get_theory; *) |
5460a5e4caa2
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
aspinall
parents:
22243
diff
changeset
|
601 |
in |
21940 | 602 |
case (thyname,objtype) of |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
603 |
(NONE, NONE) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
604 |
setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
605 |
| (NONE, SOME ObjFile) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
606 |
setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris*) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
607 |
| (SOME fi, SOME ObjFile) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
608 |
setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *) |
22225 | 609 |
| (NONE, SOME ObjTheory) => |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
610 |
setids (idtable ObjTheory NONE (ThyInfo.names())) |
22225 | 611 |
| (SOME thy, SOME ObjTheory) => |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
612 |
setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy)) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
613 |
| (SOME thy, SOME ObjTheorem) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
614 |
setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
615 |
| (NONE, SOME ObjTheorem) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
616 |
(* A large query, but not unreasonable. ~5000 results for HOL.*) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
617 |
(* Several setids should be allowed, but Eclipse code is currently broken: |
22225 | 618 |
Library.seq (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
619 |
(ThyInfo.names()) *) |
22225 | 620 |
setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
621 |
(maps qualified_thms_of_thy (ThyInfo.names()))) |
22225 | 622 |
| _ => warning ("askids: ignored argument combination") |
21637 | 623 |
end |
624 |
||
22159 | 625 |
fun askrefs (Askrefs vs) = |
626 |
let |
|
627 |
val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *) |
|
628 |
val thyname = #thyname vs (* ask for references of a theory (other theories) *) |
|
629 |
val objtype = #objtype vs (* ask for references of a particular type... *) |
|
630 |
val name = #name vs (* ... with this name *) |
|
631 |
||
632 |
fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} |
|
633 |
||
634 |
val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory |
|
635 |
||
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
636 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
22159 | 637 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
638 |
fun filerefs f = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
639 |
let val thy = thy_name f |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
640 |
val (_,filerefs) = OuterSyntax.deps_thy thy true f (* (Path.unpack f); *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
641 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
642 |
issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
643 |
name=NONE, idtables=[], fileurls=filerefs}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
644 |
end |
22159 | 645 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
646 |
fun thyrefs thy = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
647 |
let val ml_path = ThyLoad.ml_path thy |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
648 |
val (thyrefs,_) = OuterSyntax.deps_thy thy true ml_path (* (Path.unpack f); *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
649 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
650 |
issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
651 |
name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
652 |
ids=thyrefs}], fileurls=[]}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
653 |
end |
22159 | 654 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
655 |
fun thmrefs thmname = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
656 |
let |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
657 |
(* TODO: interim: this is probably not right. |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
658 |
What we want is mapping onto simple PGIP name/context model. *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
659 |
val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
660 |
val thy = Context.theory_of_proof ctx |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
661 |
val ths = [PureThy.get_thm thy (PureThy.Name thmname)] |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
662 |
val deps = filter_out (equal "") |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
663 |
(Symtab.keys (fold Proofterm.thms_of_proof |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
664 |
(map Thm.proof_of ths) Symtab.empty)) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
665 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
666 |
if null deps then () |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
667 |
else issue_pgip (Setrefs {url=url, thyname=thyname, name=name, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
668 |
objtype=SOME PgipTypes.ObjTheorem, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
669 |
idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
670 |
ids=deps}], fileurls=[]}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
671 |
end |
22159 | 672 |
in |
673 |
case (url,thyname,objtype,name) of |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
674 |
(SOME file, NONE, _, _) => filerefs file |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
675 |
| (_,SOME thy,_,_) => thyrefs thy |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
676 |
| (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname |
22159 | 677 |
| _ => error ("Unimplemented/invalid case of <askrefs>") |
678 |
end |
|
679 |
||
680 |
||
681 |
||
21940 | 682 |
fun showid (Showid vs) = |
21637 | 683 |
let |
21940 | 684 |
val thyname = #thyname vs |
685 |
val objtype = #objtype vs |
|
686 |
val name = #name vs |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
687 |
|
21940 | 688 |
val topthy = Toplevel.theory_of o Toplevel.get_state |
21637 | 689 |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
690 |
(* Decompose qualified name. FIXME: Should be a better way of doing this *) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
691 |
fun splitthy id = |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
692 |
let |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
693 |
val comps = scanwords (not o (curry op= ".")) (explode id) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
694 |
in case comps of |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
695 |
(thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
696 |
| [plainid] => (topthy(),plainid) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
697 |
| _ => raise Toplevel.UNDEF (* assert false *) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
698 |
end |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
699 |
|
21637 | 700 |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
701 |
fun idvalue strings = |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
702 |
issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
703 |
text=[XML.Elem("pgmltext",[], |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
704 |
map XML.Rawtext strings)] }) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
705 |
|
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
706 |
fun string_of_thm th = Pretty.string_of |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
707 |
(Display.pretty_thm_aux |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
708 |
(Sign.pp (Thm.theory_of_thm th)) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
709 |
false (* quote *) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
710 |
false (* show hyps *) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
711 |
[] (* asms *) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
712 |
th) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
713 |
|
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
714 |
fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name)) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
715 |
|
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
716 |
val string_of_thy = Pretty.string_of o (ProofDisplay.pretty_full_theory false) |
21940 | 717 |
in |
718 |
case (thyname, objtype) of |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
719 |
(_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)] |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
720 |
| (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name)) |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
721 |
| (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name)) |
21940 | 722 |
| (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) |
21637 | 723 |
end |
724 |
||
21867 | 725 |
(*** Inspecting state ***) |
726 |
||
21940 | 727 |
(* The file which is currently being processed interactively. |
21637 | 728 |
In the pre-PGIP code, this was informed to Isabelle and the theory loader |
729 |
on completion, but that allows for circularity in case we read |
|
730 |
ourselves. So PGIP opens the filename at the start of a script. |
|
731 |
We ought to prevent problems by modifying the theory loader to know |
|
21940 | 732 |
about this special status, but for now we just keep a local reference. |
733 |
*) |
|
21637 | 734 |
|
735 |
val currently_open_file = ref (NONE : pgipurl option) |
|
736 |
||
22163 | 737 |
fun get_currently_open_file () = ! currently_open_file; |
738 |
||
21940 | 739 |
fun askguise vs = |
21637 | 740 |
(* The "guise" is the PGIP abstraction of the prover's state. |
741 |
The <informguise> message is merely used for consistency checking. *) |
|
21940 | 742 |
let |
743 |
val openfile = !currently_open_file |
|
21637 | 744 |
|
21940 | 745 |
val topthy = Toplevel.theory_of o Toplevel.get_state |
746 |
val topthy_name = Context.theory_name o topthy |
|
21637 | 747 |
|
21940 | 748 |
val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE |
21637 | 749 |
|
21940 | 750 |
fun topproofpos () = try Toplevel.proof_position_of (Isar.state ()); |
751 |
val openproofpos = topproofpos() |
|
21637 | 752 |
in |
753 |
issue_pgip (Informguise { file = openfile, |
|
21940 | 754 |
theory = opentheory, |
755 |
(* would be nice to get thm name... *) |
|
756 |
theorem = NONE, |
|
757 |
proofpos = openproofpos }) |
|
21637 | 758 |
end |
759 |
||
21902 | 760 |
fun parsescript (Parsescript vs) = |
21637 | 761 |
let |
21940 | 762 |
val text = #text vs |
763 |
val systemdata = #systemdata vs |
|
764 |
val location = #location vs (* TODO: extract position *) |
|
21637 | 765 |
|
21867 | 766 |
val _ = start_delay_msgs () (* gather parsing errs/warns *) |
767 |
val doc = PgipParser.pgip_parser text |
|
21637 | 768 |
val errs = end_delayed_msgs () |
769 |
||
21940 | 770 |
val sysattrs = PgipTypes.opt_attr "systemdata" systemdata |
771 |
val locattrs = PgipTypes.attrs_of_location location |
|
21637 | 772 |
in |
773 |
issue_pgip (Parseresult { attrs= sysattrs@locattrs, |
|
21940 | 774 |
doc = doc, |
775 |
errs = map PgipOutput.output errs }) |
|
21637 | 776 |
end |
777 |
||
778 |
fun showproofstate vs = isarcmd "pr" |
|
779 |
||
21969 | 780 |
fun showctxt vs = isarcmd "print_context" |
21637 | 781 |
|
21902 | 782 |
fun searchtheorems (Searchtheorems vs) = |
21940 | 783 |
let |
784 |
val arg = #arg vs |
|
21637 | 785 |
in |
21969 | 786 |
isarcmd ("find_theorems " ^ arg) |
21637 | 787 |
end |
788 |
||
21940 | 789 |
fun setlinewidth (Setlinewidth vs) = |
790 |
let |
|
791 |
val width = #width vs |
|
21637 | 792 |
in |
21940 | 793 |
isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *) |
21637 | 794 |
end |
795 |
||
21902 | 796 |
fun viewdoc (Viewdoc vs) = |
21940 | 797 |
let |
798 |
val arg = #arg vs |
|
799 |
in |
|
800 |
isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *) |
|
21637 | 801 |
end |
802 |
||
21867 | 803 |
(*** Theory ***) |
804 |
||
21902 | 805 |
fun doitem (Doitem vs) = |
21637 | 806 |
let |
21940 | 807 |
val text = #text vs |
21637 | 808 |
in |
21940 | 809 |
isarcmd text |
21637 | 810 |
end |
811 |
||
812 |
fun undoitem vs = |
|
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
813 |
isarcmd "undo" |
21637 | 814 |
|
815 |
fun redoitem vs = |
|
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
816 |
isarcmd "redo" |
21637 | 817 |
|
21940 | 818 |
fun aborttheory vs = |
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
819 |
isarcmd "kill" (* was: "init_toplevel" *) |
21637 | 820 |
|
21902 | 821 |
fun retracttheory (Retracttheory vs) = |
21940 | 822 |
let |
823 |
val thyname = #thyname vs |
|
21637 | 824 |
in |
21940 | 825 |
isarcmd ("kill_thy " ^ quote thyname) |
21637 | 826 |
end |
827 |
||
21867 | 828 |
|
829 |
(*** Files ***) |
|
830 |
||
831 |
(* Path management: we allow theory files to have dependencies in |
|
832 |
their own directory, but when we change directory for a new file we |
|
833 |
remove the path. Leaving it there can cause confusion with |
|
834 |
difference in batch mode. |
|
21940 | 835 |
NB: PGIP does not assume that the prover has a load path. |
21867 | 836 |
*) |
837 |
||
838 |
local |
|
839 |
val current_working_dir = ref (NONE : string option) |
|
840 |
in |
|
21940 | 841 |
fun changecwd_dir newdirpath = |
842 |
let |
|
21867 | 843 |
val newdir = File.platform_path newdirpath |
21940 | 844 |
in |
21867 | 845 |
(case (!current_working_dir) of |
846 |
NONE => () |
|
847 |
| SOME dir => ThyLoad.del_path dir; |
|
848 |
ThyLoad.add_path newdir; |
|
849 |
current_working_dir := SOME newdir) |
|
850 |
end |
|
851 |
end |
|
852 |
||
21940 | 853 |
fun changecwd (Changecwd vs) = |
854 |
let |
|
855 |
val url = #url vs |
|
856 |
val newdir = PgipTypes.path_of_pgipurl url |
|
21867 | 857 |
in |
21940 | 858 |
changecwd_dir url |
21867 | 859 |
end |
860 |
||
21902 | 861 |
fun openfile (Openfile vs) = |
21940 | 862 |
let |
21867 | 863 |
val url = #url vs |
864 |
val filepath = PgipTypes.path_of_pgipurl url |
|
865 |
val filedir = Path.dir filepath |
|
866 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
|
867 |
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name; |
|
868 |
in |
|
869 |
case !currently_open_file of |
|
22028 | 870 |
SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^ |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
871 |
PgipTypes.string_of_pgipurl url) |
21867 | 872 |
| NONE => (openfile_retract filepath; |
21940 | 873 |
changecwd_dir filedir; |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
874 |
priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url); |
21940 | 875 |
currently_open_file := SOME url) |
21867 | 876 |
end |
877 |
||
878 |
fun closefile vs = |
|
879 |
case !currently_open_file of |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
880 |
SOME f => (proper_inform_file_processed f (Isar.state()); |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
881 |
priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); |
21867 | 882 |
currently_open_file := NONE) |
883 |
| NONE => raise PGIP ("<closefile> when no file is open!") |
|
884 |
||
21940 | 885 |
fun loadfile (Loadfile vs) = |
886 |
let |
|
887 |
val url = #url vs |
|
888 |
in |
|
22171
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
889 |
(* da: this doesn't seem to cause a problem, batch loading uses |
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
890 |
a different state context. Of course confusion is still possible, |
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
891 |
e.g. file loaded depends on open file which is not yet saved. *) |
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
892 |
(* case !currently_open_file of |
22028 | 893 |
SOME f => raise PGIP ("<loadfile> when a file is open!\nCurrently open file: " ^ |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
894 |
PgipTypes.string_of_pgipurl url) |
22171
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
895 |
| NONE => *) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
896 |
use_thy_or_ml_file (File.platform_path url) |
21637 | 897 |
end |
898 |
||
899 |
fun abortfile vs = |
|
900 |
case !currently_open_file of |
|
901 |
SOME f => (isarcmd "init_toplevel"; |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
902 |
priority ("Aborted working in file: " ^ |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
903 |
PgipTypes.string_of_pgipurl f); |
21940 | 904 |
currently_open_file := NONE) |
21637 | 905 |
| NONE => raise PGIP ("<abortfile> when no file is open!") |
906 |
||
21940 | 907 |
fun retractfile (Retractfile vs) = |
908 |
let |
|
909 |
val url = #url vs |
|
21637 | 910 |
in |
21940 | 911 |
case !currently_open_file of |
21637 | 912 |
SOME f => raise PGIP ("<retractfile> when a file is open!") |
22028 | 913 |
| NONE => (priority ("Retracting file: " ^ PgipTypes.string_of_pgipurl url); |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
914 |
(* TODO: next should be in thy loader, here just for testing *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
915 |
let |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
916 |
val name = thy_name url |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
917 |
in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end; |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
918 |
inform_file_retracted url) |
21637 | 919 |
end |
920 |
||
921 |
||
21867 | 922 |
(*** System ***) |
21637 | 923 |
|
21902 | 924 |
fun systemcmd (Systemcmd vs) = |
21940 | 925 |
let |
21637 | 926 |
val arg = #arg vs |
927 |
in |
|
928 |
isarcmd arg |
|
929 |
end |
|
930 |
||
931 |
exception PGIP_QUIT; |
|
932 |
fun quitpgip vs = raise PGIP_QUIT |
|
933 |
||
21902 | 934 |
fun process_input inp = case inp |
935 |
of Pgip.Askpgip _ => askpgip inp |
|
936 |
| Pgip.Askpgml _ => askpgml inp |
|
21940 | 937 |
| Pgip.Askprefs _ => askprefs inp |
21902 | 938 |
| Pgip.Askconfig _ => askconfig inp |
939 |
| Pgip.Getpref _ => getpref inp |
|
940 |
| Pgip.Setpref _ => setpref inp |
|
941 |
| Pgip.Proverinit _ => proverinit inp |
|
942 |
| Pgip.Proverexit _ => proverexit inp |
|
943 |
| Pgip.Startquiet _ => startquiet inp |
|
944 |
| Pgip.Stopquiet _ => stopquiet inp |
|
945 |
| Pgip.Pgmlsymbolson _ => pgmlsymbolson inp |
|
946 |
| Pgip.Pgmlsymbolsoff _ => pgmlsymbolsoff inp |
|
947 |
| Pgip.Dostep _ => dostep inp |
|
948 |
| Pgip.Undostep _ => undostep inp |
|
949 |
| Pgip.Redostep _ => redostep inp |
|
950 |
| Pgip.Forget _ => error "<forget> not implemented" |
|
951 |
| Pgip.Restoregoal _ => error "<restoregoal> not implemented" |
|
952 |
| Pgip.Abortgoal _ => abortgoal inp |
|
953 |
| Pgip.Askids _ => askids inp |
|
22159 | 954 |
| Pgip.Askrefs _ => askrefs inp |
21902 | 955 |
| Pgip.Showid _ => showid inp |
956 |
| Pgip.Askguise _ => askguise inp |
|
957 |
| Pgip.Parsescript _ => parsescript inp |
|
958 |
| Pgip.Showproofstate _ => showproofstate inp |
|
959 |
| Pgip.Showctxt _ => showctxt inp |
|
960 |
| Pgip.Searchtheorems _ => searchtheorems inp |
|
961 |
| Pgip.Setlinewidth _ => setlinewidth inp |
|
962 |
| Pgip.Viewdoc _ => viewdoc inp |
|
963 |
| Pgip.Doitem _ => doitem inp |
|
964 |
| Pgip.Undoitem _ => undoitem inp |
|
965 |
| Pgip.Redoitem _ => redoitem inp |
|
966 |
| Pgip.Aborttheory _ => aborttheory inp |
|
967 |
| Pgip.Retracttheory _ => retracttheory inp |
|
968 |
| Pgip.Loadfile _ => loadfile inp |
|
969 |
| Pgip.Openfile _ => openfile inp |
|
970 |
| Pgip.Closefile _ => closefile inp |
|
971 |
| Pgip.Abortfile _ => abortfile inp |
|
972 |
| Pgip.Retractfile _ => retractfile inp |
|
973 |
| Pgip.Changecwd _ => changecwd inp |
|
974 |
| Pgip.Systemcmd _ => systemcmd inp |
|
975 |
| Pgip.Quitpgip _ => quitpgip inp |
|
21637 | 976 |
|
977 |
||
21940 | 978 |
fun process_pgip_element pgipxml = |
21637 | 979 |
case pgipxml of |
21969 | 980 |
xml as (XML.Elem elem) => |
21940 | 981 |
(case Pgip.input elem of |
982 |
NONE => warning ("Unrecognized PGIP command, ignored: \n" ^ |
|
983 |
(XML.string_of_tree xml)) |
|
984 |
| SOME inp => (process_input inp)) (* errors later; packet discarded *) |
|
21969 | 985 |
| XML.Text t => ignored_text_warning t |
986 |
| XML.Rawtext t => ignored_text_warning t |
|
21637 | 987 |
and ignored_text_warning t = |
21940 | 988 |
if size (Symbol.strip_blanks t) > 0 then |
989 |
warning ("Ignored text in PGIP packet: \n" ^ t) |
|
21637 | 990 |
else () |
991 |
||
992 |
fun process_pgip_tree xml = |
|
993 |
(pgip_refid := NONE; |
|
994 |
pgip_refseq := NONE; |
|
995 |
(case xml of |
|
996 |
XML.Elem ("pgip", attrs, pgips) => |
|
997 |
(let |
|
998 |
val class = PgipTypes.get_attr "class" attrs |
|
999 |
val dest = PgipTypes.get_attr_opt "destid" attrs |
|
21940 | 1000 |
val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs) |
21637 | 1001 |
(* Respond to prover broadcasts, or messages for us. Ignore rest *) |
21940 | 1002 |
val processit = |
1003 |
case dest of |
|
21637 | 1004 |
NONE => class = "pa" |
21940 | 1005 |
| SOME id => matching_pgip_id id |
1006 |
in if processit then |
|
1007 |
(pgip_refid := PgipTypes.get_attr_opt "id" attrs; |
|
1008 |
pgip_refseq := SOME seq; |
|
1009 |
List.app process_pgip_element pgips; |
|
1010 |
(* return true to indicate <ready/> *) |
|
1011 |
true) |
|
1012 |
else |
|
1013 |
(* no response to ignored messages. *) |
|
1014 |
false |
|
21637 | 1015 |
end) |
1016 |
| _ => raise PGIP "Invalid PGIP packet received") |
|
1017 |
handle PGIP msg => |
|
1018 |
(Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^ |
|
21940 | 1019 |
(XML.string_of_tree xml)); |
1020 |
true)) |
|
21637 | 1021 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1022 |
(* External input *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1023 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1024 |
val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string |
21637 | 1025 |
|
1026 |
(* PGIP loop: process PGIP input only *) |
|
1027 |
||
1028 |
local |
|
1029 |
||
1030 |
exception XML_PARSE |
|
1031 |
||
1032 |
fun loop ready src = |
|
1033 |
let |
|
1034 |
val _ = if ready then issue_pgip (Ready ()) else () |
|
21969 | 1035 |
val pgipo = |
1036 |
(case try Source.get_single src of |
|
1037 |
SOME pgipo => pgipo |
|
1038 |
| NONE => raise XML_PARSE) |
|
21637 | 1039 |
in |
1040 |
case pgipo of |
|
1041 |
NONE => () |
|
1042 |
| SOME (pgip,src') => |
|
1043 |
let |
|
21940 | 1044 |
val ready' = (process_pgip_tree pgip) |
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
1045 |
handle PGIP_QUIT => raise PGIP_QUIT |
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
1046 |
| e => (handler (e,SOME src'); true) |
21637 | 1047 |
in |
1048 |
loop ready' src' |
|
1049 |
end |
|
1050 |
end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *) |
|
1051 |
||
1052 |
and handler (e,srco) = |
|
1053 |
case (e,srco) of |
|
1054 |
(XML_PARSE,SOME src) => |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
1055 |
Output.panic "Invalid XML input, aborting" (* TODO: attempt recovery *) |
21940 | 1056 |
| (Interrupt,SOME src) => |
1057 |
(Output.error_msg "Interrupt during PGIP processing"; loop true src) |
|
1058 |
| (Toplevel.UNDEF,SOME src) => |
|
1059 |
(Output.error_msg "No working context defined"; loop true src) |
|
1060 |
| (e,SOME src) => |
|
1061 |
(Output.error_msg (Toplevel.exn_message e); loop true src) |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
1062 |
| (PGIP_QUIT,_) => () |
21637 | 1063 |
| (_,NONE) => () |
1064 |
in |
|
1065 |
(* TODO: add socket interface *) |
|
1066 |
||
1067 |
val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single |
|
1068 |
||
1069 |
val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty) |
|
1070 |
||
1071 |
fun pgip_toplevel x = loop true x |
|
1072 |
end |
|
1073 |
||
1074 |
||
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1075 |
local |
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1076 |
(* Extra command for embedding prover-control inside document (obscure/debug usage). *) |
21637 | 1077 |
|
22014
4b70cbd96007
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
wenzelm
parents:
22001
diff
changeset
|
1078 |
val process_pgipP = |
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1079 |
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control |
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1080 |
(OuterParse.text >> (Toplevel.no_timing oo |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1081 |
(fn txt => Toplevel.imperative (fn () => process_pgip_plain txt)))); |
21637 | 1082 |
|
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1083 |
in |
21637 | 1084 |
|
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1085 |
fun init_outer_syntax () = OuterSyntax.add_parsers [process_pgipP]; |
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1086 |
|
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1087 |
end |
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
1088 |
|
21637 | 1089 |
|
1090 |
||
1091 |
(* init *) |
|
1092 |
||
1093 |
val initialized = ref false; |
|
1094 |
||
21969 | 1095 |
fun init_pgip false = |
1096 |
Output.panic "No Proof General interface support for Isabelle/classic mode." |
|
1097 |
| init_pgip true = |
|
1098 |
(! initialized orelse |
|
1099 |
(setmp warning_fn (K ()) init_outer_syntax (); |
|
22014
4b70cbd96007
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
wenzelm
parents:
22001
diff
changeset
|
1100 |
PgipParser.init (); |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
1101 |
setup_preferences_tweak (); |
21969 | 1102 |
setup_xsymbols_output (); |
1103 |
setup_pgml_output (); |
|
1104 |
setup_messages (); |
|
1105 |
setup_state (); |
|
1106 |
setup_thy_loader (); |
|
1107 |
setup_present_hook (); |
|
1108 |
init_pgip_session_id (); |
|
1109 |
welcome (); |
|
1110 |
set initialized); |
|
1111 |
sync_thy_loader (); |
|
1112 |
change print_mode (cons proof_generalN o remove (op =) proof_generalN); |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
1113 |
change print_mode (append [pgmlN] o subtract (op =) [pgmlN]); |
21969 | 1114 |
pgip_toplevel tty_src); |
21637 | 1115 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1116 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1117 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1118 |
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1119 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1120 |
local |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1121 |
val pgip_output_channel = ref writeln_default |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1122 |
in |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1123 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1124 |
(* Set recipient for PGIP results *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1125 |
fun init_pgip_channel writefn = |
21940 | 1126 |
(init_pgip_session_id(); |
1127 |
pgip_output_channel := writefn) |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1128 |
|
21940 | 1129 |
(* Process a PGIP command. |
1130 |
This works for preferences but not generally guaranteed |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1131 |
because we haven't done full setup here (e.g., no pgml mode) *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1132 |
fun process_pgip str = |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1133 |
setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1134 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1135 |
end |
21637 | 1136 |
|
1137 |
end; |