author | wenzelm |
Mon, 20 Sep 2010 15:08:51 +0200 | |
changeset 39555 | ccb223a4d49c |
parent 39513 | fce2202892c4 |
child 39557 | fe5722fce758 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/proof_general_pgip.ML |
2 |
Author: David Aspinall and Markus Wenzel |
|
3 |
||
4 |
Isabelle configuration for Proof General using PGIP protocol. |
|
21940 | 5 |
See http://proofgeneral.inf.ed.ac.uk/kit |
21637 | 6 |
*) |
7 |
||
8 |
signature PROOF_GENERAL_PGIP = |
|
9 |
sig |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
10 |
val proof_general_emacsN: string |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
11 |
|
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
12 |
val new_thms_deps: theory -> theory -> string list * string list |
21940 | 13 |
val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *) |
21642 | 14 |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
15 |
val pgip_channel_emacs: (string -> unit) -> unit |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
16 |
|
23435
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
17 |
(* More message functions... *) |
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
18 |
val nonfatal_error : string -> unit (* recoverable (batch) error: carry on scripting *) |
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 *) |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
20 |
val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit |
22159 | 21 |
|
22163 | 22 |
val get_currently_open_file : unit -> Path.T option (* interface focus *) |
28588 | 23 |
val add_preference: string -> Preferences.preference -> unit |
21637 | 24 |
end |
25 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
26 |
structure ProofGeneralPgip : PROOF_GENERAL_PGIP = |
21637 | 27 |
struct |
28 |
||
29 |
open Pgip; |
|
30 |
||
21949 | 31 |
|
23641
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
32 |
(** print mode **) |
21637 | 33 |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
34 |
val proof_general_emacsN = "ProofGeneralEmacs"; |
22408 | 35 |
val proof_generalN = "ProofGeneral"; |
32738 | 36 |
val pgmlsymbols_flag = Unsynchronized.ref true; |
21637 | 37 |
|
23641
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
38 |
|
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
39 |
(* assembling and issuing PGIP packets *) |
21637 | 40 |
|
32738 | 41 |
val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref; |
42 |
val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref; |
|
21637 | 43 |
|
44 |
local |
|
45 |
val pgip_class = "pg" |
|
46 |
val pgip_tag = "Isabelle/Isar" |
|
32738 | 47 |
val pgip_id = Unsynchronized.ref "" |
48 |
val pgip_seq = Unsynchronized.ref 0 |
|
49 |
fun pgip_serial () = Unsynchronized.inc pgip_seq |
|
21637 | 50 |
|
51 |
fun assemble_pgips pgips = |
|
21940 | 52 |
Pgip { tag = SOME pgip_tag, |
53 |
class = pgip_class, |
|
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
54 |
seq = pgip_serial (), |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
55 |
id = ! pgip_id, |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
56 |
destid = ! pgip_refid, |
21940 | 57 |
(* destid=refid since Isabelle only communicates back to sender *) |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
58 |
refid = ! pgip_refid, |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
59 |
refseq = ! pgip_refseq, |
21940 | 60 |
content = pgips } |
21637 | 61 |
in |
62 |
||
63 |
fun init_pgip_session_id () = |
|
64 |
pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ |
|
65 |
getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) |
|
66 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
67 |
fun matching_pgip_id id = (id = ! pgip_id) |
21637 | 68 |
|
32738 | 69 |
val output_xml_fn = Unsynchronized.ref Output.writeln_default |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
70 |
fun output_xml s = ! output_xml_fn (XML.string_of s); |
23641
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
71 |
|
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
72 |
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
73 |
|
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
74 |
val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
75 |
val output_pgmltext = XML.string_of o Pgml.pgml_to_xml; |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
76 |
|
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
77 |
|
21940 | 78 |
fun issue_pgip_rawtext str = |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
79 |
output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str))); |
21637 | 80 |
|
81 |
fun issue_pgip pgipop = |
|
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
82 |
output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop])); |
21637 | 83 |
|
84 |
end; |
|
85 |
||
86 |
||
23641
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
87 |
|
21637 | 88 |
(** messages and notification **) |
89 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
90 |
(* PGML terms *) |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
91 |
|
21637 | 92 |
local |
93 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
94 |
fun pgml_sym s = |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
95 |
if ! pgmlsymbols_flag then |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
96 |
(case Symbol.decode s of |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
97 |
Symbol.Sym name => Pgml.Sym {name = name, content = s} |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
98 |
| _ => Pgml.Str s) |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
99 |
else Pgml.Str s; |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
100 |
|
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
101 |
val pgml_syms = map pgml_sym o Symbol.explode; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
102 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
103 |
val token_markups = |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
104 |
[Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN, |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
105 |
Markup.boundN, Markup.varN, Markup.skolemN]; |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
106 |
|
21637 | 107 |
in |
108 |
||
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
109 |
fun pgml_terms (XML.Elem ((name, atts), body)) = |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
110 |
if member (op =) token_markups name then |
39555
ccb223a4d49c
added XML.content_of convenience -- cover XML.body, which is the general situation;
wenzelm
parents:
39513
diff
changeset
|
111 |
let val content = pgml_syms (XML.content_of body) |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
112 |
in [Pgml.Atoms {kind = SOME name, content = content}] end |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
113 |
else |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
114 |
let val content = maps pgml_terms body in |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
115 |
if name = Markup.blockN then |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
116 |
[Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}] |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
117 |
else if name = Markup.breakN then |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
118 |
[Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}] |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
119 |
else content |
21940 | 120 |
end |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
121 |
| pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); |
21637 | 122 |
|
123 |
end; |
|
124 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
125 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
126 |
(* messages *) |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
127 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
128 |
fun pgml area content = |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
129 |
Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content}; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
130 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
131 |
fun message_content default_area s = |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
132 |
let |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
133 |
val body = YXML.parse_body s; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
134 |
val area = |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
135 |
(case body of |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
136 |
[XML.Elem ((name, _), _)] => |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
137 |
if name = Markup.stateN then PgipTypes.Display else default_area |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
138 |
| _ => default_area); |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
139 |
in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
140 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
141 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
142 |
fun normalmsg area s = issue_pgip |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
143 |
(Normalresponse {content = [message_content area s]}); |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
144 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
145 |
fun errormsg area fatality s = issue_pgip |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
146 |
(Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]}); |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
147 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
148 |
(*error responses with useful locations*) |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
149 |
fun error_with_pos area fatality pos s = issue_pgip |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
150 |
(Errorresponse { |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
151 |
fatality = fatality, |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
152 |
location = SOME (PgipIsabelle.location_of_position pos), |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
153 |
content = [message_content area s]}); |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
154 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
155 |
fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1); |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
156 |
fun nonfatal_error s = errormsg Message Nonfatal s; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
157 |
fun log_msg s = errormsg Message Log s; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
158 |
|
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
159 |
(* NB: 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
|
160 |
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
|
161 |
can't be written without newlines. *) |
21637 | 162 |
fun setup_messages () = |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
163 |
(Output.writeln_fn := (fn s => normalmsg Message s); |
27604 | 164 |
Output.status_fn := (fn _ => ()); |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38228
diff
changeset
|
165 |
Output.report_fn := (fn _ => ()); |
23840 | 166 |
Output.priority_fn := (fn s => normalmsg Status s); |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
167 |
Output.tracing_fn := (fn s => normalmsg Tracing s); |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
168 |
Output.warning_fn := (fn s => errormsg Message Warning s); |
39513
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
39232
diff
changeset
|
169 |
Output.error_fn := (fn s => errormsg Message Fatal s)); |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
170 |
|
21637 | 171 |
|
172 |
(* immediate messages *) |
|
173 |
||
26706 | 174 |
fun tell_clear_goals () = |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
175 |
issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Display [])] }) |
26706 | 176 |
fun tell_clear_response () = |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
177 |
issue_pgip (Normalresponse { content = [Pgml.pgml_to_xml (pgml Message [])] }) |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
178 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
179 |
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
|
180 |
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
|
181 |
completed=completed}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
182 |
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
|
183 |
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
|
184 |
completed=completed}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
185 |
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
|
186 |
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
|
187 |
completed=completed}) |
21637 | 188 |
|
189 |
||
190 |
(* theory loader actions *) |
|
191 |
||
192 |
local |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
193 |
(* 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
|
194 |
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
|
195 |
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
|
196 |
(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
|
197 |
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
|
198 |
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
|
199 |
operations). |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
200 |
*) |
21637 | 201 |
fun trace_action action name = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
202 |
if action = Thy_Info.Update then |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
203 |
List.app (tell_file_loaded true) (Thy_Info.loaded_files name) |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
204 |
else if action = Thy_Info.Remove then |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
205 |
List.app (tell_file_retracted true) (Thy_Info.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
|
206 |
else () |
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
207 |
|
21637 | 208 |
|
209 |
in |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
210 |
fun setup_thy_loader () = Thy_Info.add_hook trace_action; |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
211 |
fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ()); |
21637 | 212 |
end; |
213 |
||
214 |
||
21949 | 215 |
(* get informed about files *) |
21637 | 216 |
|
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
217 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base; |
21637 | 218 |
|
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37954
diff
changeset
|
219 |
val inform_file_retracted = Thy_Info.kill_thy o thy_name; |
21637 | 220 |
|
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset
|
221 |
fun inform_file_processed path state = |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
222 |
let val name = thy_name path in |
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37954
diff
changeset
|
223 |
if Toplevel.is_toplevel state then |
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset
|
224 |
Thy_Info.register_thy (Toplevel.end_theory Position.none state) |
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset
|
225 |
handle ERROR msg => |
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset
|
226 |
(warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); |
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset
|
227 |
tell_file_retracted true (Path.base path)) |
21637 | 228 |
else raise Toplevel.UNDEF |
229 |
end; |
|
230 |
||
231 |
||
232 |
(* restart top-level loop (keeps most state information) *) |
|
233 |
||
234 |
val welcome = priority o Session.welcome; |
|
235 |
||
236 |
fun restart () = |
|
237 |
(sync_thy_loader (); |
|
238 |
tell_clear_goals (); |
|
239 |
tell_clear_response (); |
|
29349 | 240 |
Isar.init (); |
27578 | 241 |
welcome ()); |
21637 | 242 |
|
243 |
||
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
244 |
(* theorem dependencies *) |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
245 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
246 |
local |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
247 |
|
28809 | 248 |
fun add_proof_body (PBody {thms, ...}) = |
28817 | 249 |
thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ())); |
28809 | 250 |
|
251 |
fun add_thm th = |
|
28814 | 252 |
(case Thm.proof_body_of th of |
28809 | 253 |
PBody {proof = PThm (_, ((name, _, _), body)), ...} => |
254 |
if Thm.has_name_hint th andalso Thm.get_name_hint th = name |
|
29635
31d14e9fa0da
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29606
diff
changeset
|
255 |
then add_proof_body (Future.join body) |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
256 |
else I |
28809 | 257 |
| body => add_proof_body body); |
258 |
||
259 |
in |
|
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
260 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
261 |
fun thms_deps ths = |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
262 |
let |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
263 |
(* FIXME proper derivation names!? *) |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
264 |
val names = map Thm.get_name_hint (filter Thm.has_name_hint ths); |
28809 | 265 |
val deps = Symtab.keys (fold add_thm ths Symtab.empty); |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
266 |
in (names, deps) end; |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
267 |
|
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
268 |
fun new_thms_deps thy thy' = |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
269 |
let |
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
270 |
val prev_facts = PureThy.facts_of thy; |
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
271 |
val facts = PureThy.facts_of thy'; |
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
272 |
in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end; |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
273 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
274 |
end; |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
275 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
276 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
277 |
(* theorem dependeny output *) |
22408 | 278 |
|
32738 | 279 |
val show_theorem_dependencies = Unsynchronized.ref false; |
22408 | 280 |
|
21637 | 281 |
local |
282 |
||
283 |
val spaces_quote = space_implode " " o map quote; |
|
284 |
||
285 |
fun thm_deps_message (thms, deps) = |
|
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
286 |
let |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
287 |
val valuethms = XML.Elem (("value", [("name", "thms")]), [XML.Text thms]); |
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
288 |
val valuedeps = XML.Elem (("value", [("name", "deps")]), [XML.Text deps]); |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
289 |
in |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
290 |
issue_pgip (Metainforesponse |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
291 |
{attrs = [("infotype", "isabelle_theorem_dependencies")], |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
292 |
content = [valuethms, valuedeps]}) |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
293 |
end; |
21637 | 294 |
|
295 |
in |
|
296 |
||
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28100
diff
changeset
|
297 |
fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' => |
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
298 |
if ! show_theorem_dependencies andalso |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28100
diff
changeset
|
299 |
can Toplevel.theory_of state andalso Toplevel.is_theory state' |
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
300 |
then |
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
301 |
let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
302 |
if null names orelse null deps then () |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
303 |
else thm_deps_message (spaces_quote names, spaces_quote deps) |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
304 |
end |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
305 |
else ()); |
21637 | 306 |
|
307 |
end; |
|
308 |
||
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
309 |
|
21637 | 310 |
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **) |
311 |
||
21940 | 312 |
fun lexicalstructure_keywords () = |
36950 | 313 |
let val keywords = Keyword.dest_keywords () |
314 |
val commands = Keyword.dest_commands () |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27177
diff
changeset
|
315 |
fun keyword_elt kind keyword = |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
316 |
XML.Elem (("keyword", [("word", keyword), ("category", kind)]), []) |
21940 | 317 |
in |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27177
diff
changeset
|
318 |
Lexicalstructure |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27177
diff
changeset
|
319 |
{content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands} |
21637 | 320 |
end |
321 |
||
322 |
(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically; |
|
323 |
hooks needed in outer_syntax.ML to do that. *) |
|
324 |
||
325 |
||
326 |
(* Configuration: GUI config, proverinfo messages *) |
|
327 |
||
328 |
local |
|
329 |
val isabellewww = "http://isabelle.in.tum.de/" |
|
330 |
val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml" |
|
21940 | 331 |
fun orenv v d = case getenv v of "" => d | s => s |
21637 | 332 |
fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig |
333 |
fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww |
|
334 |
in |
|
335 |
fun send_pgip_config () = |
|
336 |
let |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21655
diff
changeset
|
337 |
val path = Path.explode (config_file()) |
21940 | 338 |
val ex = File.exists path |
21637 | 339 |
|
21940 | 340 |
val wwwpage = |
341 |
(Url.explode (isabelle_www())) |
|
21969 | 342 |
handle ERROR _ => |
22699
938c1011ac94
removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents:
22678
diff
changeset
|
343 |
(panic ("Error in URL in environment variable ISABELLE_HOMEPAGE."); |
21940 | 344 |
Url.explode isabellewww) |
345 |
||
346 |
val proverinfo = |
|
21637 | 347 |
Proverinfo { name = "Isabelle", |
26109
c69c3559355b
more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents:
25847
diff
changeset
|
348 |
version = Distribution.version, |
21940 | 349 |
instance = Session.name(), |
350 |
descr = "The Isabelle/Isar theorem prover", |
|
351 |
url = wwwpage, |
|
352 |
filenameextns = ".thy;" } |
|
21637 | 353 |
in |
21940 | 354 |
if ex then |
355 |
(issue_pgip proverinfo; |
|
356 |
issue_pgip_rawtext (File.read path); |
|
357 |
issue_pgip (lexicalstructure_keywords())) |
|
22699
938c1011ac94
removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents:
22678
diff
changeset
|
358 |
else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found") |
21637 | 359 |
end; |
360 |
end |
|
361 |
||
362 |
||
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
|
363 |
(* 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
|
364 |
|
32738 | 365 |
val preferences = Unsynchronized.ref Preferences.pure_preferences; |
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
|
366 |
|
28066
611e504c1191
extended interface to preferences to allow adding new ones
nipkow
parents:
28037
diff
changeset
|
367 |
fun add_preference cat pref = |
32738 | 368 |
CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref)); |
28066
611e504c1191
extended interface to preferences to allow adding new ones
nipkow
parents:
28037
diff
changeset
|
369 |
|
28588 | 370 |
fun setup_preferences_tweak () = |
32738 | 371 |
CRITICAL (fn () => Unsynchronized.change preferences |
28588 | 372 |
(Preferences.set_default ("show-question-marks", "false") #> |
373 |
Preferences.remove "show-question-marks" #> (* we use markup, not ?s *) |
|
374 |
Preferences.remove "theorem-dependencies" #> (* set internally *) |
|
375 |
Preferences.remove "full-proofs")); (* set internally *) |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
376 |
|
21637 | 377 |
|
378 |
||
379 |
(* Sending commands to Isar *) |
|
380 |
||
36953
2af1ad9aa1a3
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
381 |
fun isarcmd s = Isar.>>> (Outer_Syntax.parse Position.none s); |
21637 | 382 |
|
21940 | 383 |
(* TODO: |
27565 | 384 |
- apply a command given a transition function; |
21885
5a11263bd8cf
Remove obsolete prefixes from error and warning messages.
aspinall
parents:
21867
diff
changeset
|
385 |
- 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
|
386 |
*) |
21637 | 387 |
|
388 |
(* load an arbitrary file (must be .thy or .ML) *) |
|
389 |
||
390 |
fun use_thy_or_ml_file file = |
|
391 |
let |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21655
diff
changeset
|
392 |
val (path,extn) = Path.split_ext (Path.explode file) |
21637 | 393 |
in |
394 |
case extn of |
|
21940 | 395 |
"" => isarcmd ("use_thy " ^ quote (Path.implode path)) |
396 |
| "thy" => isarcmd ("use_thy " ^ quote (Path.implode path)) |
|
21637 | 397 |
| "ML" => isarcmd ("use " ^ quote file) |
22028 | 398 |
| other => error ("Don't know how to read a file with extension " ^ quote other) |
21637 | 399 |
end |
400 |
||
401 |
||
21867 | 402 |
(******* PGIP actions *******) |
21637 | 403 |
|
404 |
||
21940 | 405 |
(* Responses to each of the PGIP input commands. |
21637 | 406 |
These are programmed uniformly for extensibility. *) |
407 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
408 |
fun askpgip (Askpgip _) = |
23435
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
409 |
(issue_pgip |
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
410 |
(Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported, |
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
411 |
pgipelems = PgipIsabelle.accepted_inputs }); |
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
412 |
send_pgip_config()) |
21637 | 413 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
414 |
fun askpgml (Askpgml _) = |
21637 | 415 |
issue_pgip |
21940 | 416 |
(Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported }) |
21637 | 417 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
418 |
fun askprefs (Askprefs _) = |
21940 | 419 |
let |
420 |
fun preference_of {name, descr, default, pgiptype, get, set } = |
|
421 |
{ name = name, descr = SOME descr, default = SOME default, |
|
422 |
pgiptype = pgiptype } |
|
21637 | 423 |
in |
21940 | 424 |
List.app (fn (prefcat, prefs) => |
425 |
issue_pgip (Hasprefs {prefcategory=SOME prefcat, |
|
426 |
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
|
427 |
(!preferences) |
21940 | 428 |
end |
21637 | 429 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
430 |
fun askconfig (Askconfig _) = () (* TODO: add config response *) |
21637 | 431 |
|
432 |
local |
|
21940 | 433 |
fun lookuppref pref = |
434 |
case AList.lookup (op =) |
|
435 |
(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
|
436 |
(maps snd (!preferences))) pref of |
21940 | 437 |
NONE => error ("Unknown prover preference: " ^ quote pref) |
438 |
| SOME p => p |
|
21637 | 439 |
in |
21940 | 440 |
fun setpref (Setpref vs) = |
441 |
let |
|
442 |
val name = #name vs |
|
443 |
val value = #value vs |
|
444 |
val set = #set (lookuppref name) |
|
21637 | 445 |
in |
21940 | 446 |
set value |
21637 | 447 |
end |
448 |
||
21902 | 449 |
fun getpref (Getpref vs) = |
21940 | 450 |
let |
451 |
val name = #name vs |
|
452 |
val get = #get (lookuppref name) |
|
453 |
in |
|
21637 | 454 |
issue_pgip (Prefval {name=name, value=get ()}) |
455 |
end |
|
456 |
end |
|
457 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
458 |
fun proverinit _ = restart () |
21637 | 459 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
460 |
fun proverexit _ = isarcmd "quit" |
21637 | 461 |
|
26706 | 462 |
fun set_proverflag_quiet b = |
22408 | 463 |
isarcmd (if b then "disable_pr" else "enable_pr") |
21637 | 464 |
|
22408 | 465 |
fun set_proverflag_pgmlsymbols b = |
466 |
(pgmlsymbols_flag := b; |
|
24614 | 467 |
NAMED_CRITICAL "print_mode" (fn () => |
32738 | 468 |
Unsynchronized.change print_mode |
22590 | 469 |
(fn mode => |
24614 | 470 |
remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))) |
22408 | 471 |
|
472 |
fun set_proverflag_thmdeps b = |
|
473 |
(show_theorem_dependencies := b; |
|
25223 | 474 |
Proofterm.proofs := (if b then 1 else 2)) |
21637 | 475 |
|
22408 | 476 |
fun setproverflag (Setproverflag vs) = |
26706 | 477 |
let |
22590 | 478 |
val flagname = #flagname vs |
479 |
val value = #value vs |
|
22408 | 480 |
in |
22590 | 481 |
(case flagname of |
482 |
"quiet" => set_proverflag_quiet value |
|
483 |
| "pgmlsymbols" => set_proverflag_pgmlsymbols value |
|
26706 | 484 |
| "metainfo:thmdeps" => set_proverflag_thmdeps value |
485 |
| _ => log_msg ("Unrecognised prover control flag: " ^ |
|
23801 | 486 |
(quote flagname) ^ " ignored.")) |
26706 | 487 |
end |
22408 | 488 |
|
21637 | 489 |
|
21940 | 490 |
fun dostep (Dostep vs) = |
491 |
let |
|
492 |
val text = #text vs |
|
493 |
in |
|
494 |
isarcmd text |
|
21637 | 495 |
end |
496 |
||
21902 | 497 |
fun undostep (Undostep vs) = |
21940 | 498 |
let |
499 |
val times = #times vs |
|
500 |
in |
|
501 |
isarcmd ("undos_proof " ^ Int.toString times) |
|
21637 | 502 |
end |
503 |
||
37852
a902f158b4fc
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37216
diff
changeset
|
504 |
fun redostep _ = raise Fail "redo unavailable" |
21940 | 505 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
506 |
fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *) |
21637 | 507 |
|
508 |
||
21867 | 509 |
(*** PGIP identifier tables ***) |
510 |
||
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
511 |
(* TODO: these ones should be triggered by hooks after a |
22159 | 512 |
declaration addition/removal, to be sent automatically. *) |
21867 | 513 |
|
22159 | 514 |
fun addids t = issue_pgip (Addids {idtables = [t]}) |
515 |
fun delids t = issue_pgip (Delids {idtables = [t]}) |
|
21867 | 516 |
|
27177 | 517 |
|
518 |
local |
|
519 |
||
520 |
fun theory_facts name = |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
521 |
let val thy = Thy_Info.get_theory name |
27177 | 522 |
in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end; |
523 |
||
524 |
fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static); |
|
525 |
fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static); |
|
526 |
||
527 |
in |
|
528 |
||
21940 | 529 |
fun askids (Askids vs) = |
21637 | 530 |
let |
21940 | 531 |
val url = #url vs (* ask for identifiers within a file *) |
532 |
val thyname = #thyname vs (* ask for identifiers within a theory *) |
|
533 |
val objtype = #objtype vs (* ask for identifiers of a particular type *) |
|
21867 | 534 |
|
21940 | 535 |
fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} |
21867 | 536 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
537 |
fun setids t = issue_pgip (Setids {idtables = [t]}) |
22159 | 538 |
|
22225 | 539 |
(* fake one-level nested "subtheories" by picking apart names. *) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
29635
diff
changeset
|
540 |
val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
29635
diff
changeset
|
541 |
fun thy_prefix s = case Long_Name.explode s of |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
542 |
x::_::_ => SOME x (* String.find? *) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
543 |
| _ => NONE |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
544 |
fun subthys_of_thy s = |
23178 | 545 |
List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) [] |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
546 |
(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
|
547 |
fun subthms_of_thy thy = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
548 |
(case thy_prefix thy of |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
549 |
NONE => immed_thms_of_thy thy |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
29635
diff
changeset
|
550 |
| SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy)) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
551 |
(thms_of_thy prf)) |
26706 | 552 |
in |
21940 | 553 |
case (thyname,objtype) of |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
554 |
(NONE, NONE) => |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
555 |
setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
556 |
| (NONE, SOME ObjFile) => |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
557 |
setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
558 |
| (SOME fi, SOME ObjFile) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
559 |
setids (idtable ObjTheory (SOME fi) [fi]) (* TODO: check exists *) |
22225 | 560 |
| (NONE, SOME ObjTheory) => |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
561 |
setids (idtable ObjTheory NONE (Thy_Info.get_names())) |
22225 | 562 |
| (SOME thy, SOME ObjTheory) => |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
563 |
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
|
564 |
| (SOME thy, SOME ObjTheorem) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
565 |
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
|
566 |
| (NONE, SOME ObjTheorem) => |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
567 |
(* 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
|
568 |
(* Several setids should be allowed, but Eclipse code is currently broken: |
23226 | 569 |
List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy))) |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
570 |
(Thy_Info.get_names()) *) |
22225 | 571 |
setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *) |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
572 |
(maps qualified_thms_of_thy (Thy_Info.get_names()))) |
22225 | 573 |
| _ => warning ("askids: ignored argument combination") |
21637 | 574 |
end |
575 |
||
27177 | 576 |
end; |
577 |
||
22159 | 578 |
fun askrefs (Askrefs vs) = |
579 |
let |
|
580 |
val url = #url vs (* ask for references of a file (i.e. immediate pre-requisites) *) |
|
581 |
val thyname = #thyname vs (* ask for references of a theory (other theories) *) |
|
582 |
val objtype = #objtype vs (* ask for references of a particular type... *) |
|
583 |
val name = #name vs (* ... with this name *) |
|
584 |
||
585 |
fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} |
|
586 |
||
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
587 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
22159 | 588 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
589 |
fun filerefs f = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
590 |
let val thy = thy_name f |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
591 |
val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
592 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
593 |
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
|
594 |
name=NONE, idtables=[], fileurls=filerefs}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
595 |
end |
22159 | 596 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
597 |
fun thyrefs thy = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
598 |
let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
599 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
600 |
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
|
601 |
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
|
602 |
ids=thyrefs}], fileurls=[]}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
603 |
end |
22159 | 604 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
605 |
fun thmrefs thmname = |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
606 |
let |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
607 |
(* 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
|
608 |
What we want is mapping onto simple PGIP name/context model. *) |
26603 | 609 |
val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *) |
33030 | 610 |
val thy = ProofContext.theory_of ctx |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
611 |
val ths = [PureThy.get_thm thy thmname] |
28809 | 612 |
val deps = #2 (thms_deps ths); |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
613 |
in |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
614 |
if null deps then () |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
615 |
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
|
616 |
objtype=SOME PgipTypes.ObjTheorem, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
617 |
idtables=[{context=NONE, objtype=PgipTypes.ObjTheorem, |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
618 |
ids=deps}], fileurls=[]}) |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
619 |
end |
22159 | 620 |
in |
621 |
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
|
622 |
(SOME file, NONE, _, _) => filerefs file |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
623 |
| (_,SOME thy,_,_) => thyrefs thy |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
624 |
| (_,_,SOME PgipTypes.ObjTheorem,SOME thmname) => thmrefs thmname |
22159 | 625 |
| _ => error ("Unimplemented/invalid case of <askrefs>") |
626 |
end |
|
627 |
||
628 |
||
629 |
||
21940 | 630 |
fun showid (Showid vs) = |
21637 | 631 |
let |
21940 | 632 |
val thyname = #thyname vs |
633 |
val objtype = #objtype vs |
|
634 |
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
|
635 |
|
26603 | 636 |
val topthy = Toplevel.theory_of o Isar.state |
21637 | 637 |
|
22590 | 638 |
fun splitthy id = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
29635
diff
changeset
|
639 |
let val comps = Long_Name.explode id |
22590 | 640 |
in case comps of |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
641 |
(thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest) |
22590 | 642 |
| [plainid] => (topthy(),plainid) |
643 |
| _ => raise Toplevel.UNDEF (* assert false *) |
|
26706 | 644 |
end |
645 |
||
21637 | 646 |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
647 |
fun idvalue strings = |
26706 | 648 |
issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, |
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
649 |
text=[XML.Elem (("pgml", []), maps YXML.parse_body strings)] }) |
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
650 |
|
32144 | 651 |
fun strings_of_thm (thy, name) = |
652 |
map (Display.string_of_thm_global thy) (PureThy.get_thms thy name) |
|
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
653 |
|
33389 | 654 |
val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false |
21940 | 655 |
in |
656 |
case (thyname, objtype) of |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
657 |
(_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)] |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
658 |
| (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name)) |
22337
d4599c206446
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
aspinall
parents:
22249
diff
changeset
|
659 |
| (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name)) |
21940 | 660 |
| (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) |
21637 | 661 |
end |
662 |
||
21867 | 663 |
(*** Inspecting state ***) |
664 |
||
21940 | 665 |
(* The file which is currently being processed interactively. |
21637 | 666 |
In the pre-PGIP code, this was informed to Isabelle and the theory loader |
667 |
on completion, but that allows for circularity in case we read |
|
668 |
ourselves. So PGIP opens the filename at the start of a script. |
|
669 |
We ought to prevent problems by modifying the theory loader to know |
|
21940 | 670 |
about this special status, but for now we just keep a local reference. |
671 |
*) |
|
21637 | 672 |
|
32738 | 673 |
val currently_open_file = Unsynchronized.ref (NONE : pgipurl option) |
21637 | 674 |
|
22163 | 675 |
fun get_currently_open_file () = ! currently_open_file; |
676 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
677 |
fun askguise _ = |
21637 | 678 |
(* The "guise" is the PGIP abstraction of the prover's state. |
679 |
The <informguise> message is merely used for consistency checking. *) |
|
21940 | 680 |
let |
681 |
val openfile = !currently_open_file |
|
21637 | 682 |
|
26603 | 683 |
val topthy = Toplevel.theory_of o Isar.state |
21940 | 684 |
val topthy_name = Context.theory_name o topthy |
21637 | 685 |
|
21940 | 686 |
val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE |
21637 | 687 |
|
21940 | 688 |
fun topproofpos () = try Toplevel.proof_position_of (Isar.state ()); |
689 |
val openproofpos = topproofpos() |
|
21637 | 690 |
in |
691 |
issue_pgip (Informguise { file = openfile, |
|
21940 | 692 |
theory = opentheory, |
693 |
(* would be nice to get thm name... *) |
|
694 |
theorem = NONE, |
|
695 |
proofpos = openproofpos }) |
|
21637 | 696 |
end |
697 |
||
21902 | 698 |
fun parsescript (Parsescript vs) = |
21637 | 699 |
let |
21940 | 700 |
val text = #text vs |
701 |
val systemdata = #systemdata vs |
|
702 |
val location = #location vs (* TODO: extract position *) |
|
21637 | 703 |
|
28020 | 704 |
val doc = PgipParser.pgip_parser Position.none text |
21637 | 705 |
|
21940 | 706 |
val sysattrs = PgipTypes.opt_attr "systemdata" systemdata |
707 |
val locattrs = PgipTypes.attrs_of_location location |
|
21637 | 708 |
in |
709 |
issue_pgip (Parseresult { attrs= sysattrs@locattrs, |
|
21940 | 710 |
doc = doc, |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
711 |
errs = [] }) |
21637 | 712 |
end |
713 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
714 |
fun showproofstate _ = isarcmd "pr" |
21637 | 715 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
716 |
fun showctxt _ = isarcmd "print_context" |
21637 | 717 |
|
21902 | 718 |
fun searchtheorems (Searchtheorems vs) = |
21940 | 719 |
let |
720 |
val arg = #arg vs |
|
21637 | 721 |
in |
21969 | 722 |
isarcmd ("find_theorems " ^ arg) |
21637 | 723 |
end |
724 |
||
21940 | 725 |
fun setlinewidth (Setlinewidth vs) = |
726 |
let |
|
727 |
val width = #width vs |
|
21637 | 728 |
in |
21940 | 729 |
isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *) |
21637 | 730 |
end |
731 |
||
21902 | 732 |
fun viewdoc (Viewdoc vs) = |
21940 | 733 |
let |
734 |
val arg = #arg vs |
|
735 |
in |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28443
diff
changeset
|
736 |
isarcmd ("print_" ^ arg) (* FIXME: isabelle doc?. Return URLs, maybe? *) |
21637 | 737 |
end |
738 |
||
21867 | 739 |
(*** Theory ***) |
740 |
||
21902 | 741 |
fun doitem (Doitem vs) = |
21637 | 742 |
let |
21940 | 743 |
val text = #text vs |
21637 | 744 |
in |
21940 | 745 |
isarcmd text |
21637 | 746 |
end |
747 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
748 |
fun undoitem _ = |
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
749 |
isarcmd "undo" |
21637 | 750 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
751 |
fun redoitem _ = |
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
752 |
isarcmd "redo" |
21637 | 753 |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
754 |
fun aborttheory _ = |
21972
1b68312c4cf0
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
aspinall
parents:
21970
diff
changeset
|
755 |
isarcmd "kill" (* was: "init_toplevel" *) |
21637 | 756 |
|
21902 | 757 |
fun retracttheory (Retracttheory vs) = |
21940 | 758 |
let |
759 |
val thyname = #thyname vs |
|
21637 | 760 |
in |
21940 | 761 |
isarcmd ("kill_thy " ^ quote thyname) |
21637 | 762 |
end |
763 |
||
21867 | 764 |
|
765 |
(*** Files ***) |
|
766 |
||
767 |
(* Path management: we allow theory files to have dependencies in |
|
768 |
their own directory, but when we change directory for a new file we |
|
769 |
remove the path. Leaving it there can cause confusion with |
|
770 |
difference in batch mode. |
|
21940 | 771 |
NB: PGIP does not assume that the prover has a load path. |
21867 | 772 |
*) |
773 |
||
774 |
local |
|
32738 | 775 |
val current_working_dir = Unsynchronized.ref (NONE : string option) |
21867 | 776 |
in |
21940 | 777 |
fun changecwd_dir newdirpath = |
778 |
let |
|
21867 | 779 |
val newdir = File.platform_path newdirpath |
21940 | 780 |
in |
21867 | 781 |
(case (!current_working_dir) of |
782 |
NONE => () |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
783 |
| SOME dir => Thy_Load.del_path dir; |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
784 |
Thy_Load.add_path newdir; |
21867 | 785 |
current_working_dir := SOME newdir) |
786 |
end |
|
787 |
end |
|
788 |
||
21940 | 789 |
fun changecwd (Changecwd vs) = |
790 |
let |
|
791 |
val url = #url vs |
|
792 |
val newdir = PgipTypes.path_of_pgipurl url |
|
21867 | 793 |
in |
21940 | 794 |
changecwd_dir url |
21867 | 795 |
end |
796 |
||
21902 | 797 |
fun openfile (Openfile vs) = |
21940 | 798 |
let |
21867 | 799 |
val url = #url vs |
800 |
val filepath = PgipTypes.path_of_pgipurl url |
|
801 |
val filedir = Path.dir filepath |
|
802 |
val thy_name = Path.implode o #1 o Path.split_ext o Path.base |
|
38833
9ff5ce3580c1
eliminated obsolete Output.no_warnings, where no warnings were produced anyway;
wenzelm
parents:
38798
diff
changeset
|
803 |
val openfile_retract = Thy_Info.kill_thy o thy_name; |
21867 | 804 |
in |
805 |
case !currently_open_file of |
|
22028 | 806 |
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
|
807 |
PgipTypes.string_of_pgipurl url) |
21867 | 808 |
| NONE => (openfile_retract filepath; |
21940 | 809 |
changecwd_dir filedir; |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
810 |
priority ("Working in file: " ^ PgipTypes.string_of_pgipurl url); |
21940 | 811 |
currently_open_file := SOME url) |
21867 | 812 |
end |
813 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
814 |
fun closefile _ = |
21867 | 815 |
case !currently_open_file of |
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset
|
816 |
SOME f => (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
|
817 |
priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f); |
21867 | 818 |
currently_open_file := NONE) |
819 |
| NONE => raise PGIP ("<closefile> when no file is open!") |
|
820 |
||
21940 | 821 |
fun loadfile (Loadfile vs) = |
822 |
let |
|
823 |
val url = #url vs |
|
824 |
in |
|
22171
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
825 |
(* 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
|
826 |
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
|
827 |
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
|
828 |
(* case !currently_open_file of |
22028 | 829 |
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
|
830 |
PgipTypes.string_of_pgipurl url) |
22171
58f554f51f0d
Let <loadfile> execute even while a file is open interactively.
aspinall
parents:
22163
diff
changeset
|
831 |
| NONE => *) |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
832 |
use_thy_or_ml_file (File.platform_path url) |
21637 | 833 |
end |
834 |
||
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
835 |
fun abortfile _ = |
21637 | 836 |
case !currently_open_file of |
837 |
SOME f => (isarcmd "init_toplevel"; |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
838 |
priority ("Aborted working in file: " ^ |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
839 |
PgipTypes.string_of_pgipurl f); |
21940 | 840 |
currently_open_file := NONE) |
21637 | 841 |
| NONE => raise PGIP ("<abortfile> when no file is open!") |
842 |
||
21940 | 843 |
fun retractfile (Retractfile vs) = |
844 |
let |
|
845 |
val url = #url vs |
|
21637 | 846 |
in |
21940 | 847 |
case !currently_open_file of |
21637 | 848 |
SOME f => raise PGIP ("<retractfile> when a file is open!") |
22028 | 849 |
| 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
|
850 |
(* 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
|
851 |
let |
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
852 |
val name = thy_name url |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset
|
853 |
in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end; |
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
854 |
inform_file_retracted url) |
21637 | 855 |
end |
856 |
||
857 |
||
21867 | 858 |
(*** System ***) |
21637 | 859 |
|
21902 | 860 |
fun systemcmd (Systemcmd vs) = |
21940 | 861 |
let |
21637 | 862 |
val arg = #arg vs |
863 |
in |
|
864 |
isarcmd arg |
|
865 |
end |
|
866 |
||
867 |
exception PGIP_QUIT; |
|
23834
ad6ad61332fa
avoid redundant variables in patterns (which made Alice vomit);
wenzelm
parents:
23801
diff
changeset
|
868 |
fun quitpgip _ = raise PGIP_QUIT |
21637 | 869 |
|
21902 | 870 |
fun process_input inp = case inp |
871 |
of Pgip.Askpgip _ => askpgip inp |
|
872 |
| Pgip.Askpgml _ => askpgml inp |
|
21940 | 873 |
| Pgip.Askprefs _ => askprefs inp |
21902 | 874 |
| Pgip.Askconfig _ => askconfig inp |
875 |
| Pgip.Getpref _ => getpref inp |
|
876 |
| Pgip.Setpref _ => setpref inp |
|
877 |
| Pgip.Proverinit _ => proverinit inp |
|
878 |
| Pgip.Proverexit _ => proverexit inp |
|
22408 | 879 |
| Pgip.Setproverflag _ => setproverflag inp |
21902 | 880 |
| Pgip.Dostep _ => dostep inp |
881 |
| Pgip.Undostep _ => undostep inp |
|
882 |
| Pgip.Redostep _ => redostep inp |
|
23435
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
883 |
| Pgip.Forget _ => error "<forget> not implemented by Isabelle" |
061f28854017
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
aspinall
parents:
23226
diff
changeset
|
884 |
| Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle" |
21902 | 885 |
| Pgip.Abortgoal _ => abortgoal inp |
886 |
| Pgip.Askids _ => askids inp |
|
22159 | 887 |
| Pgip.Askrefs _ => askrefs inp |
21902 | 888 |
| Pgip.Showid _ => showid inp |
889 |
| Pgip.Askguise _ => askguise inp |
|
890 |
| Pgip.Parsescript _ => parsescript inp |
|
891 |
| Pgip.Showproofstate _ => showproofstate inp |
|
892 |
| Pgip.Showctxt _ => showctxt inp |
|
893 |
| Pgip.Searchtheorems _ => searchtheorems inp |
|
894 |
| Pgip.Setlinewidth _ => setlinewidth inp |
|
895 |
| Pgip.Viewdoc _ => viewdoc inp |
|
896 |
| Pgip.Doitem _ => doitem inp |
|
897 |
| Pgip.Undoitem _ => undoitem inp |
|
898 |
| Pgip.Redoitem _ => redoitem inp |
|
899 |
| Pgip.Aborttheory _ => aborttheory inp |
|
900 |
| Pgip.Retracttheory _ => retracttheory inp |
|
901 |
| Pgip.Loadfile _ => loadfile inp |
|
902 |
| Pgip.Openfile _ => openfile inp |
|
903 |
| Pgip.Closefile _ => closefile inp |
|
904 |
| Pgip.Abortfile _ => abortfile inp |
|
905 |
| Pgip.Retractfile _ => retractfile inp |
|
906 |
| Pgip.Changecwd _ => changecwd inp |
|
907 |
| Pgip.Systemcmd _ => systemcmd inp |
|
908 |
| Pgip.Quitpgip _ => quitpgip inp |
|
21637 | 909 |
|
910 |
||
21940 | 911 |
fun process_pgip_element pgipxml = |
21637 | 912 |
case pgipxml of |
21969 | 913 |
xml as (XML.Elem elem) => |
21940 | 914 |
(case Pgip.input elem of |
915 |
NONE => warning ("Unrecognized PGIP command, ignored: \n" ^ |
|
26541 | 916 |
(XML.string_of xml)) |
21940 | 917 |
| SOME inp => (process_input inp)) (* errors later; packet discarded *) |
21969 | 918 |
| XML.Text t => ignored_text_warning t |
21637 | 919 |
and ignored_text_warning t = |
21940 | 920 |
if size (Symbol.strip_blanks t) > 0 then |
921 |
warning ("Ignored text in PGIP packet: \n" ^ t) |
|
21637 | 922 |
else () |
923 |
||
924 |
fun process_pgip_tree xml = |
|
925 |
(pgip_refid := NONE; |
|
926 |
pgip_refseq := NONE; |
|
927 |
(case xml of |
|
38228
ada3ab6b9085
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents:
37981
diff
changeset
|
928 |
XML.Elem (("pgip", attrs), pgips) => |
21637 | 929 |
(let |
930 |
val class = PgipTypes.get_attr "class" attrs |
|
931 |
val dest = PgipTypes.get_attr_opt "destid" attrs |
|
21940 | 932 |
val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs) |
21637 | 933 |
(* Respond to prover broadcasts, or messages for us. Ignore rest *) |
21940 | 934 |
val processit = |
935 |
case dest of |
|
21637 | 936 |
NONE => class = "pa" |
21940 | 937 |
| SOME id => matching_pgip_id id |
938 |
in if processit then |
|
939 |
(pgip_refid := PgipTypes.get_attr_opt "id" attrs; |
|
940 |
pgip_refseq := SOME seq; |
|
941 |
List.app process_pgip_element pgips; |
|
942 |
(* return true to indicate <ready/> *) |
|
943 |
true) |
|
944 |
else |
|
945 |
(* no response to ignored messages. *) |
|
946 |
false |
|
21637 | 947 |
end) |
948 |
| _ => raise PGIP "Invalid PGIP packet received") |
|
949 |
handle PGIP msg => |
|
36148 | 950 |
(Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^ |
26541 | 951 |
(XML.string_of xml)); |
21940 | 952 |
true)) |
21637 | 953 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
954 |
(* External input *) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
955 |
|
26541 | 956 |
val process_pgip_plain = K () o process_pgip_tree o XML.parse |
21637 | 957 |
|
958 |
(* PGIP loop: process PGIP input only *) |
|
959 |
||
960 |
local |
|
961 |
||
962 |
exception XML_PARSE |
|
963 |
||
964 |
fun loop ready src = |
|
965 |
let |
|
966 |
val _ = if ready then issue_pgip (Ready ()) else () |
|
21969 | 967 |
val pgipo = |
968 |
(case try Source.get_single src of |
|
969 |
SOME pgipo => pgipo |
|
970 |
| NONE => raise XML_PARSE) |
|
21637 | 971 |
in |
972 |
case pgipo of |
|
973 |
NONE => () |
|
974 |
| SOME (pgip,src') => |
|
975 |
let |
|
21940 | 976 |
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
|
977 |
handle PGIP_QUIT => raise PGIP_QUIT |
22590 | 978 |
| e => (handler (e,SOME src'); true) |
21637 | 979 |
in |
980 |
loop ready' src' |
|
981 |
end |
|
982 |
end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *) |
|
983 |
||
984 |
and handler (e,srco) = |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
985 |
if Exn.is_interrupt e andalso is_some srco then |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
986 |
(Output.error_msg "Interrupt during PGIP processing"; loop true (the srco)) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
987 |
else |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
988 |
case (e,srco) of |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
989 |
(XML_PARSE,SOME src) => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
990 |
panic "Invalid XML input, aborting" (* TODO: attempt recovery *) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
991 |
| (Toplevel.UNDEF,SOME src) => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
992 |
(Output.error_msg "No working context defined"; loop true src) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
993 |
| (e,SOME src) => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
994 |
(Output.error_msg (ML_Compiler.exn_message e); loop true src) |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
995 |
| (PGIP_QUIT,_) => () |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
39139
diff
changeset
|
996 |
| (_,NONE) => () |
21637 | 997 |
in |
998 |
(* TODO: add socket interface *) |
|
999 |
||
26552
5677b4faf295
renamed XML.parse_comment_whspc to XML.parse_comments;
wenzelm
parents:
26548
diff
changeset
|
1000 |
val xmlP = XML.parse_comments |-- XML.parse_element >> single |
21637 | 1001 |
|
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
1002 |
val tty_src = |
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
1003 |
Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE (Source.tty TextIO.stdIn)) |
21637 | 1004 |
|
1005 |
fun pgip_toplevel x = loop true x |
|
1006 |
end |
|
1007 |
||
1008 |
||
1009 |
(* init *) |
|
1010 |
||
32738 | 1011 |
val initialized = Unsynchronized.ref false; |
21637 | 1012 |
|
22699
938c1011ac94
removed unused Output.panic hook -- internal to PG wrapper;
wenzelm
parents:
22678
diff
changeset
|
1013 |
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode." |
21969 | 1014 |
| init_pgip true = |
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
38253
diff
changeset
|
1015 |
(if ! initialized then () |
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
38253
diff
changeset
|
1016 |
else |
25445
01f3686f4304
Init outer syntax after message setup to avoid spurious output.
aspinall
parents:
25275
diff
changeset
|
1017 |
(setup_preferences_tweak (); |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
1018 |
Output.add_mode proof_generalN Output.default_output Output.default_escape; |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
1019 |
Markup.add_mode proof_generalN YXML.output_markup; |
25445
01f3686f4304
Init outer syntax after message setup to avoid spurious output.
aspinall
parents:
25275
diff
changeset
|
1020 |
setup_messages (); |
01f3686f4304
Init outer syntax after message setup to avoid spurious output.
aspinall
parents:
25275
diff
changeset
|
1021 |
setup_thy_loader (); |
01f3686f4304
Init outer syntax after message setup to avoid spurious output.
aspinall
parents:
25275
diff
changeset
|
1022 |
setup_present_hook (); |
01f3686f4304
Init outer syntax after message setup to avoid spurious output.
aspinall
parents:
25275
diff
changeset
|
1023 |
init_pgip_session_id (); |
01f3686f4304
Init outer syntax after message setup to avoid spurious output.
aspinall
parents:
25275
diff
changeset
|
1024 |
welcome (); |
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
38253
diff
changeset
|
1025 |
initialized := true); |
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
38253
diff
changeset
|
1026 |
sync_thy_loader (); |
32738 | 1027 |
Unsynchronized.change print_mode (update (op =) proof_generalN); |
21969 | 1028 |
pgip_toplevel tty_src); |
21637 | 1029 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1030 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1031 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1032 |
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **) |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1033 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1034 |
local |
32738 | 1035 |
val pgip_output_channel = Unsynchronized.ref Output.writeln_default |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1036 |
in |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1037 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1038 |
(* Set recipient for PGIP results *) |
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1039 |
fun pgip_channel_emacs writefn = |
21940 | 1040 |
(init_pgip_session_id(); |
1041 |
pgip_output_channel := writefn) |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1042 |
|
21940 | 1043 |
(* Process a PGIP command. |
1044 |
This works for preferences but not generally guaranteed |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1045 |
because we haven't done full setup here (e.g., no pgml mode) *) |
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1046 |
fun process_pgip_emacs str = |
39139
8235606e2b23
use setmp_noncritical for PGIP, which is presumably sequential (PG clone);
wenzelm
parents:
38837
diff
changeset
|
1047 |
setmp_noncritical output_xml_fn (!pgip_output_channel) process_pgip_plain str |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1048 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
1049 |
end |
21637 | 1050 |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1051 |
|
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1052 |
(* Extra command for embedding prover-control inside document (obscure/debug usage). *) |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1053 |
|
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1054 |
val _ = |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1055 |
Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1056 |
(Parse.text >> (Toplevel.no_timing oo |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1057 |
(fn txt => Toplevel.imperative (fn () => |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1058 |
if print_mode_active proof_general_emacsN |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1059 |
then process_pgip_emacs txt |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1060 |
else process_pgip_plain txt)))); |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
1061 |
|
21637 | 1062 |
end; |