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