author | wenzelm |
Thu, 01 Sep 2005 15:58:08 +0200 | |
changeset 17217 | 954c0f265203 |
parent 17057 | 0934ac31985f |
child 17221 | 6cd180204582 |
permissions | -rw-r--r-- |
12780 | 1 |
(* Title: Pure/proof_general.ML |
12778 | 2 |
ID: $Id$ |
14675 | 3 |
Author: David Aspinall and Markus Wenzel |
12778 | 4 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
5 |
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
6 |
Includes support for PGIP control language for Isabelle/Isar. |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
7 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
8 |
=========================================================================== |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
9 |
NOTE: With this version you will lose support for the Isabelle |
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
10 |
settings menu in the currently released version of Proof General (3.5). |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
11 |
No other changes should be visible in the Emacs interface. |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
12 |
|
16534 | 13 |
The 3.6pre pre-release versions of Emacs Proof General now support the |
14 |
new PGIP format for preferences and restore the settings menu. |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
15 |
Please visit http://proofgeneral.inf.ed.ac.uk/develdownload |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
16 |
=========================================================================== |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
17 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
18 |
STATUS: this version is an experimental version that supports PGIP 2.X. |
12778 | 19 |
*) |
20 |
||
21 |
signature PROOF_GENERAL = |
|
22 |
sig |
|
23 |
val update_thy_only: string -> unit |
|
24 |
val try_update_thy_only: string -> unit |
|
13391 | 25 |
val inform_file_retracted: string -> unit |
12778 | 26 |
val inform_file_processed: string -> unit |
16534 | 27 |
val preferences: |
28 |
(string * |
|
29 |
(string * |
|
30 |
(string * |
|
31 |
(string * (string * (unit -> string)) * |
|
32 |
(string -> unit)))) list) list ref |
|
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
33 |
val process_pgip: string -> unit |
12778 | 34 |
val thms_containing: string list -> unit |
35 |
val help: unit -> unit |
|
36 |
val show_context: unit -> theory |
|
37 |
val kill_goal: unit -> unit |
|
38 |
val repeat_undo: int -> unit |
|
39 |
val isa_restart: unit -> unit |
|
12833 | 40 |
val full_proofs: bool -> unit |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
41 |
val isarcmd: string -> unit |
12778 | 42 |
val init: bool -> unit |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
43 |
val init_pgip: bool -> unit |
12778 | 44 |
val write_keywords: string -> unit |
16534 | 45 |
val xmls_of_str: string -> string list (*temp for testing parser*) |
12778 | 46 |
end; |
47 |
||
16534 | 48 |
structure ProofGeneral: PROOF_GENERAL = |
12778 | 49 |
struct |
50 |
||
16534 | 51 |
structure P = OuterParse; |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
52 |
|
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
53 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
54 |
(* PGIP messaging mode (independent of PGML output) *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
55 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
56 |
val pgip_active = ref false; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
57 |
val pgip_emacs_compatibility_flag = ref false; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
58 |
|
16534 | 59 |
fun pgip () = (! pgip_active); |
60 |
fun pgip_emacs_compatibility () = (! pgip_emacs_compatibility_flag); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
61 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
62 |
|
12778 | 63 |
(* print modes *) |
64 |
||
16534 | 65 |
val proof_generalN = "ProofGeneral"; (*token markup (colouring vars, etc.)*) |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
66 |
val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*) |
16534 | 67 |
val xsymbolsN = Symbol.xsymbolsN; (*X-Symbol symbols*) |
68 |
val pgmlN = "PGML"; (*XML escapes and PGML symbol elements*) |
|
69 |
val pgmlatomsN = "PGMLatoms"; (*variable kind decorations*) |
|
70 |
val thm_depsN = "thm_deps"; (*meta-information about theorem deps*) |
|
12778 | 71 |
|
16534 | 72 |
fun pgml () = Output.has_mode pgmlN; |
73 |
||
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
74 |
fun special oct = |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
75 |
if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
76 |
else oct_char oct; |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
77 |
|
12778 | 78 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
79 |
(* text output: print modes for xsymbol and PGML *) |
12778 | 80 |
|
81 |
local |
|
82 |
||
14827 | 83 |
fun xsym_output "\\" = "\\\\" |
84 |
| xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; |
|
85 |
||
12778 | 86 |
fun xsymbols_output s = |
16534 | 87 |
if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then |
12778 | 88 |
let val syms = Symbol.explode s |
14827 | 89 |
in (implode (map xsym_output syms), real (Symbol.length syms)) end |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
90 |
else Symbol.default_output s; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
91 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
92 |
fun pgml_sym s = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
93 |
(case Symbol.decode s of |
16534 | 94 |
(*NB: an alternative here would be to output the default print mode alternative |
95 |
in the element content, but unfortunately print modes are not that fine grained.*) |
|
15266 | 96 |
Symbol.Char s => XML.text s |
15403 | 97 |
| Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s] |
16534 | 98 |
| Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *) |
15266 | 99 |
| Symbol.Raw s => s); |
12778 | 100 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
101 |
fun pgml_output str = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
102 |
let val syms = Symbol.explode str |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
103 |
in (implode (map pgml_sym syms), real (Symbol.length syms)) end; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
104 |
|
16534 | 105 |
in |
12778 | 106 |
|
16534 | 107 |
fun setup_xsymbols_output () = |
108 |
Output.add_mode xsymbolsN |
|
109 |
(xsymbols_output, Symbol.default_indent, Symbol.encode_raw); |
|
12778 | 110 |
|
16534 | 111 |
fun setup_pgml_output () = |
112 |
Output.add_mode pgmlN |
|
113 |
(pgml_output, Symbol.default_indent, Symbol.encode_raw); |
|
12778 | 114 |
|
115 |
end; |
|
116 |
||
117 |
||
118 |
(* token translations *) |
|
119 |
||
120 |
local |
|
121 |
||
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
122 |
fun end_tag () = special "350"; |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
123 |
val class_tag = ("class", fn () => special "351"); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
124 |
val tfree_tag = ("tfree", fn () => special "352"); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
125 |
val tvar_tag = ("tvar", fn () => special "353"); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
126 |
val free_tag = ("free", fn () => special "354"); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
127 |
val bound_tag = ("bound", fn () => special "355"); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
128 |
val var_tag = ("var", fn () => special "356"); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
129 |
val skolem_tag = ("skolem", fn () => special "357"); |
12778 | 130 |
|
131 |
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; |
|
132 |
||
133 |
fun tagit (kind, bg_tag) x = |
|
16534 | 134 |
(if Output.has_mode pgmlatomsN then xml_atom kind x |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
135 |
else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x))); |
12778 | 136 |
|
137 |
fun free_or_skolem x = |
|
138 |
(case try Syntax.dest_skolem x of |
|
15531 | 139 |
NONE => tagit free_tag x |
140 |
| SOME x' => tagit skolem_tag x'); |
|
12778 | 141 |
|
142 |
fun var_or_skolem s = |
|
15985 | 143 |
(case Syntax.read_variable s of |
144 |
SOME (x, i) => |
|
12778 | 145 |
(case try Syntax.dest_skolem x of |
15531 | 146 |
NONE => tagit var_tag s |
15992
cb02d70a2040
var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents:
15985
diff
changeset
|
147 |
| SOME x' => tagit skolem_tag |
cb02d70a2040
var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents:
15985
diff
changeset
|
148 |
(setmp show_question_marks true Syntax.string_of_vname (x', i))) |
15985 | 149 |
| NONE => tagit var_tag s); |
12778 | 150 |
|
151 |
val proof_general_trans = |
|
152 |
Syntax.tokentrans_mode proof_generalN |
|
153 |
[("class", tagit class_tag), |
|
154 |
("tfree", tagit tfree_tag), |
|
155 |
("tvar", tagit tvar_tag), |
|
156 |
("free", free_or_skolem), |
|
157 |
("bound", tagit bound_tag), |
|
158 |
("var", var_or_skolem)]; |
|
159 |
||
15801 | 160 |
in |
161 |
||
162 |
val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans]; |
|
163 |
||
164 |
end; |
|
12778 | 165 |
|
166 |
||
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
167 |
(* assembling PGIP packets *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
168 |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
169 |
val pgip_refid = ref NONE: string option ref; |
16534 | 170 |
val pgip_refseq = ref NONE: string option ref; |
12778 | 171 |
|
172 |
local |
|
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
173 |
val pgip_class = "pg" |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
174 |
val pgip_tag = "Isabelle/Isar" |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
175 |
val pgip_id = ref "" |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
176 |
val pgip_seq = ref 0 |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
177 |
fun pgip_serial () = inc pgip_seq |
12778 | 178 |
|
16534 | 179 |
fun assemble_pgips pgips = |
180 |
XML.element |
|
181 |
"pgip" |
|
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
182 |
([("tag", pgip_tag), |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
183 |
("class", pgip_class), |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
184 |
("seq", string_of_int (pgip_serial())), |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
185 |
("id", !pgip_id)] @ |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
186 |
if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @ |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
187 |
(* destid=refid since Isabelle only communicates back to sender, |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
188 |
so we may omit refid from attributes. |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
189 |
if_none (Option.map (single o (pair "refid")) (! pgip_refid)) [] @ |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
190 |
*) |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
191 |
if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) []) |
16534 | 192 |
pgips; |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
193 |
|
13526 | 194 |
in |
12778 | 195 |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
196 |
fun init_pgip_session_id () = |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
197 |
pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
198 |
getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
199 |
|
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
200 |
|
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
201 |
fun matching_pgip_id id = (id = !pgip_id) |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
202 |
|
16534 | 203 |
fun decorated_output bg en prfx = |
204 |
writeln_default o enclose bg en o prefix_lines prfx; |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
205 |
|
16534 | 206 |
(* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used |
207 |
for PG 4.0 which processes PGIP without needing special chars *) |
|
208 |
fun issue_pgips ps = |
|
209 |
if pgip_emacs_compatibility() then |
|
210 |
decorated_output (*add urgent message annotation*) |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
211 |
(special "360") (special "361") "" |
16534 | 212 |
(assemble_pgips ps) |
213 |
else |
|
214 |
writeln_default (assemble_pgips ps); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
215 |
|
16534 | 216 |
fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]; |
217 |
fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]; |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
218 |
|
16534 | 219 |
(* FIXME: need to add stuff to gather PGIPs here *) |
220 |
fun issue_pgip resp attrs txt = |
|
221 |
if pgip_emacs_compatibility () then |
|
222 |
decorated_output (*add urgent message annotation*) |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
223 |
(special "360") (special "361") "" |
16534 | 224 |
(assemble_pgip resp attrs txt) |
225 |
else |
|
226 |
writeln_default (assemble_pgip resp attrs txt); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
227 |
|
16534 | 228 |
(* FIXME: temporarily to support PG 3.4 *) |
229 |
fun issue_pgip_maybe_decorated bg en resp attrs s = |
|
230 |
if pgip_emacs_compatibility () then |
|
231 |
(*in PGIP mode, but using escape characters as well*) |
|
232 |
writeln_default (enclose bg en (assemble_pgip resp attrs s)) |
|
233 |
else |
|
234 |
issue_pgip resp attrs s; |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
235 |
|
16534 | 236 |
fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs); |
237 |
||
238 |
end; |
|
239 |
||
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
240 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
241 |
(* messages and notification *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
242 |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
243 |
local |
16534 | 244 |
val delay_msgs = ref false; (*true: accumulate messages*) |
245 |
val delayed_msgs = ref []; |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
246 |
in |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
247 |
|
16534 | 248 |
fun message resp attrs bg en prfx s = |
249 |
if pgip () then |
|
250 |
(if (! delay_msgs) then |
|
251 |
delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*) |
|
252 |
else |
|
253 |
issue_pgip_maybe_decorated bg en resp attrs |
|
254 |
(XML.element "pgmltext" [] [prefix_lines prfx s])) |
|
255 |
else decorated_output bg en prfx s; |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
256 |
|
16534 | 257 |
fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []); |
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
258 |
|
16534 | 259 |
fun end_delayed_msgs () = (reset delay_msgs; |
260 |
(! delayed_msgs) |> map (fn (resp, attrs, s) => |
|
261 |
XML.element resp attrs [XML.element "pgmltext" [] [s]])); |
|
262 |
||
263 |
end; |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
264 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
265 |
local |
16534 | 266 |
val display_area = ("area", "display"); |
267 |
val message_area = ("area", "message"); |
|
268 |
val internal_category = ("messagecategory", "internal"); |
|
269 |
val info_category = ("messagecategory", "information"); |
|
270 |
val tracing_category = ("messagecategory", "tracing"); |
|
271 |
val urgent_indication = ("urgent", "y"); |
|
272 |
val nonfatal = ("fatality", "nonfatal"); |
|
273 |
val fatal = ("fatality", "fatal"); |
|
274 |
val panic = ("fatality", "panic"); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
275 |
|
16534 | 276 |
val thyname_attr = pair "thyname"; |
277 |
val url_attr = pair "url"; |
|
278 |
fun localfile_url_attr path = url_attr ("file:///" ^ path); |
|
279 |
in |
|
12778 | 280 |
|
281 |
fun setup_messages () = |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
282 |
(writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
283 |
priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
284 |
(special "360") (special "361") "" s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
285 |
tracing_fn := (fn s => message "normalresponse" [message_area, tracing_category] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
286 |
(special "360" ^ special "375") (special "361") "" s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
287 |
info_fn := (fn s => message "normalresponse" [message_area, info_category] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
288 |
(special "362") (special "363") "+++ " s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
289 |
debug_fn := (fn s => message "normalresponse" [message_area, internal_category] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
290 |
(special "362") (special "363") "+++ " s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
291 |
warning_fn := (fn s => message "errorresponse" [nonfatal] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
292 |
(special "362") (special "363") "### " s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
293 |
error_fn := (fn s => message "errorresponse" [fatal] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
294 |
(special "364") (special "365") "*** " s); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
295 |
panic_fn := (fn s => message "errorresponse" [panic] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
296 |
(special "364") (special "365") "!!! " s)); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
297 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
298 |
|
15400
50bbdabd7326
Insert pgmltext element into responses in PGIP mode
aspinall
parents:
15289
diff
changeset
|
299 |
(* accumulate printed output in a single PGIP response (inside <pgmltext>) *) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
300 |
|
16534 | 301 |
fun with_displaywrap (elt, attrs) dispfn = |
302 |
let |
|
303 |
val lines = ref ([]: string list); |
|
304 |
fun wlgrablines s = lines := s :: ! lines; |
|
305 |
in |
|
306 |
setmp writeln_fn wlgrablines dispfn (); |
|
16798 | 307 |
(* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *) |
16534 | 308 |
issue_pgip elt attrs (XML.element "pgmltext" [] (! lines)) |
309 |
end; |
|
12778 | 310 |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
311 |
fun emacs_notify s = decorated_output (special "360") (special "361") "" s; |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
312 |
|
16534 | 313 |
fun tell_clear_goals () = |
314 |
if pgip () then |
|
315 |
issue_pgipe "cleardisplay" [display_area] |
|
316 |
else |
|
317 |
emacs_notify "Proof General, please clear the goals buffer."; |
|
318 |
||
319 |
fun tell_clear_response () = |
|
320 |
if pgip () then |
|
321 |
issue_pgipe "cleardisplay" [message_area] |
|
322 |
else |
|
323 |
emacs_notify "Proof General, please clear the response buffer."; |
|
12778 | 324 |
|
16534 | 325 |
fun tell_file_loaded path = |
326 |
if pgip () then |
|
16788
0c6f5fe30676
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents:
16534
diff
changeset
|
327 |
issue_pgipe "informfileloaded" |
0c6f5fe30676
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents:
16534
diff
changeset
|
328 |
[localfile_url_attr (XML.text (File.platform_path path))] |
16534 | 329 |
else |
330 |
emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path)); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
331 |
|
16534 | 332 |
fun tell_file_retracted path = |
333 |
if pgip() then |
|
16788
0c6f5fe30676
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents:
16534
diff
changeset
|
334 |
issue_pgipe "informfileretracted" |
0c6f5fe30676
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents:
16534
diff
changeset
|
335 |
[localfile_url_attr (XML.text (File.platform_path path))] |
16534 | 336 |
else |
337 |
emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path)); |
|
12778 | 338 |
|
339 |
||
340 |
(* theory / proof state output *) |
|
341 |
||
342 |
local |
|
343 |
||
16534 | 344 |
fun tmp_markers f = |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
345 |
setmp Display.current_goals_markers (special "366", special "367", "") f (); |
12778 | 346 |
|
16534 | 347 |
fun statedisplay prts = |
348 |
issue_pgip "proofstate" [] |
|
349 |
(XML.element "pgml" [] |
|
350 |
[XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]); |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
351 |
|
16534 | 352 |
fun print_current_goals n m st = |
353 |
if pgml () then statedisplay (Display.pretty_current_goals n m st) |
|
354 |
else tmp_markers (fn () => Display.print_current_goals_default n m st); |
|
13545 | 355 |
|
16534 | 356 |
fun print_state b st = |
357 |
if pgml () then statedisplay (Toplevel.pretty_state b st) |
|
358 |
else tmp_markers (fn () => Toplevel.print_state_default b st); |
|
359 |
||
13526 | 360 |
in |
361 |
||
16534 | 362 |
fun setup_state () = |
363 |
(Display.print_current_goals_fn := print_current_goals; |
|
364 |
Toplevel.print_state_fn := print_state; |
|
365 |
(* FIXME: check next octal char won't appear in pgip? *) |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
366 |
Toplevel.prompt_state_fn := (fn s => suffix (special "372") |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
367 |
(Toplevel.prompt_state_default s))); |
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
368 |
|
16534 | 369 |
end; |
370 |
||
371 |
end; |
|
13728
8004e56204fd
Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents:
13646
diff
changeset
|
372 |
|
16022 | 373 |
|
12778 | 374 |
(* misc commands for ProofGeneral/isa *) |
375 |
||
376 |
fun thms_containing ss = |
|
16534 | 377 |
FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE |
16022 | 378 |
(map (fn s => (true, FindTheorems.Pattern s)) ss); |
12778 | 379 |
|
380 |
val welcome = priority o Session.welcome; |
|
381 |
val help = welcome; |
|
382 |
val show_context = Context.the_context; |
|
383 |
||
384 |
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ()); |
|
385 |
||
386 |
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f; |
|
387 |
||
388 |
fun repeat_undo 0 = () |
|
389 |
| repeat_undo 1 = undo () |
|
390 |
| repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1)); |
|
391 |
||
392 |
||
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
393 |
(* theory loader actions *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
394 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
395 |
local |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
396 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
397 |
fun add_master_files name files = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
398 |
let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name] |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
399 |
in masters @ gen_rems (op = o pairself Path.base) (files, masters) end; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
400 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
401 |
fun trace_action action name = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
402 |
if action = ThyInfo.Update then |
15570 | 403 |
List.app tell_file_loaded (ThyInfo.loaded_files name) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
404 |
else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then |
15570 | 405 |
List.app tell_file_retracted (add_master_files name (ThyInfo.loaded_files name)) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
406 |
else (); |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
407 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
408 |
in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
409 |
fun setup_thy_loader () = ThyInfo.add_hook trace_action; |
15570 | 410 |
fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ()); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
411 |
end; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
412 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
413 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
414 |
(* prepare theory context *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
415 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
416 |
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack; |
16534 | 417 |
|
418 |
(* FIXME general treatment of tracing*) |
|
419 |
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only; |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
420 |
|
16440 | 421 |
fun dynamic_context () = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
422 |
(case Context.get_context () of |
16440 | 423 |
SOME thy => " Using current (dynamic!) one: " ^ quote (Context.theory_name thy) |
15531 | 424 |
| NONE => ""); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
425 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
426 |
fun try_update_thy_only file = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
427 |
ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () => |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
428 |
let val name = thy_name file in |
16534 | 429 |
if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name)) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
430 |
then update_thy_only name |
16440 | 431 |
else warning ("Unkown theory context of ML file." ^ dynamic_context ()) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
432 |
end) (); |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
433 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
434 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
435 |
(* get informed about files *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
436 |
|
16534 | 437 |
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; |
438 |
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name; |
|
439 |
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name; |
|
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
440 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
441 |
fun proper_inform_file_processed file state = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
442 |
let val name = thy_name file in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
443 |
if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
444 |
(ThyInfo.touch_child_thys name; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
445 |
transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg => |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
446 |
(warning msg; warning ("Failed to register theory: " ^ quote name); |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
447 |
tell_file_retracted (Path.base (Path.unpack file)))) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
448 |
else raise Toplevel.UNDEF |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
449 |
end; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
450 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
451 |
fun vacuous_inform_file_processed file state = |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
452 |
(warning ("No theory " ^ quote (thy_name file)); |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
453 |
tell_file_retracted (Path.base (Path.unpack file))); |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
454 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
455 |
|
12778 | 456 |
(* restart top-level loop (keeps most state information) *) |
457 |
||
458 |
local |
|
459 |
||
460 |
fun restart isar = |
|
461 |
(if isar then tell_clear_goals () else kill_goal (); |
|
462 |
tell_clear_response (); |
|
463 |
welcome ()); |
|
464 |
||
465 |
in |
|
466 |
||
467 |
fun isa_restart () = restart false; |
|
468 |
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART); |
|
469 |
||
470 |
end; |
|
471 |
||
12833 | 472 |
fun full_proofs true = proofs := 2 |
473 |
| full_proofs false = proofs := 1; |
|
474 |
||
475 |
||
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
476 |
(* theorem dependency output *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
477 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
478 |
local |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
479 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
480 |
val spaces_quote = space_implode " " o map quote; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
481 |
|
16789
e8f7a6ec92e5
Note about theorem dependencies including themselves.
aspinall
parents:
16788
diff
changeset
|
482 |
(* FIXME: investigate why dependencies at the moment include themselves! *) |
16534 | 483 |
fun thm_deps_message (thms, deps) = |
484 |
if pgip() then |
|
485 |
issue_pgips |
|
486 |
[XML.element |
|
487 |
"metainforesponse" (* FIXME: get thy name from info here? *) |
|
488 |
[("infotype", "isabelle_theorem_dependencies")] |
|
489 |
[XML.element "value" [("name", "thms")] [XML.text thms], |
|
490 |
XML.element "value" [("name", "deps")] [XML.text deps]]] |
|
491 |
else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
492 |
|
16534 | 493 |
fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () => |
494 |
let |
|
495 |
val names = filter_out (equal "") (map Thm.name_of_thm ths); |
|
496 |
val deps = filter_out (equal "") |
|
17018 | 497 |
(Symtab.keys (fold Proofterm.thms_of_proof |
498 |
(map Thm.proof_of ths) Symtab.empty)); |
|
16534 | 499 |
in |
500 |
if null names orelse null deps then () |
|
501 |
else thm_deps_message (spaces_quote names, spaces_quote deps) |
|
502 |
end); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
503 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
504 |
in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
505 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
506 |
fun setup_present_hook () = |
15570 | 507 |
Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res))); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
508 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
509 |
end; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
510 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
511 |
|
16534 | 512 |
|
513 |
(** preferences **) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
514 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
515 |
local |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
516 |
|
16534 | 517 |
val pgipnat = XML.element "pgipint" [("min", "0")] []; |
518 |
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] []; |
|
519 |
val pgipbool = XML.element "pgipbool" [] []; |
|
520 |
||
521 |
fun with_default f = (f (), f); |
|
522 |
||
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
523 |
in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
524 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
525 |
fun nat_option r = (pgipnat, |
16534 | 526 |
with_default (fn () => string_of_int (! r)), |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
527 |
(fn s => (case Syntax.read_nat s of |
16534 | 528 |
NONE => error ("nat_option: illegal value: " ^ s) |
529 |
| SOME i => r := i))); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
530 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
531 |
fun bool_option r = (pgipbool, |
16534 | 532 |
with_default (fn () => Bool.toString (! r)), |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
533 |
(fn "false" => r := false | "true" => r := true |
16534 | 534 |
| x => error ("bool_option: illegal value: " ^ x))); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
535 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
536 |
val proof_option = (pgipbool, |
16534 | 537 |
with_default (fn () => Bool.toString (! proofs >= 2)), |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
538 |
(fn "false" => proofs := 1 | "true" => proofs := 2 |
16534 | 539 |
| x => error ("proof_option: illegal value: " ^ x))); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
540 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
541 |
val thm_deps_option = (pgipbool, |
16534 | 542 |
with_default (fn () => Bool.toString (Output.has_mode thm_depsN)), |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
543 |
(fn "false" => change print_mode (remove (op =) thm_depsN) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
544 |
| "true" => change print_mode (insert (op =) thm_depsN) |
16534 | 545 |
| x => error ("thm_deps_option: illegal value: " ^ x))); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
546 |
|
16534 | 547 |
local |
548 |
val pg_print_depth_val = ref 10; |
|
549 |
fun pg_print_depth n = (print_depth n; pg_print_depth_val := n) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
550 |
in |
16534 | 551 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
552 |
val print_depth_option = (pgipnat, |
16534 | 553 |
with_default (fn () => string_of_int (! pg_print_depth_val)), |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
554 |
(fn s => (case Syntax.read_nat s of |
16534 | 555 |
NONE => error ("print_depth_option: illegal value: " ^ s) |
556 |
| SOME i => pg_print_depth i))); |
|
557 |
end; |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
558 |
|
16534 | 559 |
val preferences = ref |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
560 |
[("Display", |
16534 | 561 |
[("show-types", |
562 |
("Include types in display of Isabelle terms", |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
563 |
bool_option show_types)), |
16534 | 564 |
("show-sorts", |
565 |
("Include sorts in display of Isabelle terms", |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
566 |
bool_option show_sorts)), |
16534 | 567 |
("show-consts", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
568 |
("Show types of consts in Isabelle goal display", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
569 |
bool_option show_consts)), |
16534 | 570 |
("long-names", |
571 |
("Show fully qualified names in Isabelle terms", |
|
572 |
bool_option long_names)), |
|
573 |
("show-brackets", |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
574 |
("Show full bracketing in Isabelle terms", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
575 |
bool_option show_brackets)), |
16534 | 576 |
("show-main-goal", |
577 |
("Show main goal in proof state display", |
|
578 |
bool_option Proof.show_main_goal)), |
|
579 |
("eta-contract", |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
580 |
("Print terms eta-contracted", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
581 |
bool_option Syntax.eta_contract))]), |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
582 |
("Advanced Display", |
16534 | 583 |
[("goals-limit", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
584 |
("Setting for maximum number of goals printed", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
585 |
nat_option goals_limit)), |
16534 | 586 |
("prems-limit", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
587 |
("Setting for maximum number of premises printed", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
588 |
nat_option ProofContext.prems_limit)), |
16534 | 589 |
("print-depth", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
590 |
("Setting for the ML print depth", |
15472 | 591 |
print_depth_option)), |
15985 | 592 |
("show-question-marks", |
15472 | 593 |
("Show leading question mark of variable name", |
15985 | 594 |
bool_option show_question_marks))]), |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
595 |
("Tracing", |
16534 | 596 |
[("trace-simplifier", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
597 |
("Trace simplification rules.", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
598 |
bool_option trace_simp)), |
16534 | 599 |
("trace-rules", |
600 |
("Trace application of the standard rules", |
|
601 |
bool_option trace_rules)), |
|
602 |
("trace-unification", |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
603 |
("Output error diagnostics during unification", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
604 |
bool_option Pattern.trace_unify_fail)), |
16534 | 605 |
("global-timing", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
606 |
("Whether to enable timing in Isabelle.", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
607 |
bool_option Output.timing))]), |
16534 | 608 |
("Proof", |
609 |
[("quick-and-dirty", |
|
610 |
("Take a few short cuts", |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
611 |
bool_option quick_and_dirty)), |
16534 | 612 |
("full-proofs", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
613 |
("Record full proof objects internally", |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
614 |
proof_option)), |
16534 | 615 |
("theorem-dependencies", |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
616 |
("Track theorem dependencies within Proof General", |
16534 | 617 |
thm_deps_option)), |
618 |
("skip-proofs", |
|
16816 | 619 |
("Ignore proof scripts (interactive-only)", |
15238
cb559bd0b03c
Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents:
15225
diff
changeset
|
620 |
bool_option Toplevel.skip_proofs))]) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
621 |
]; |
16534 | 622 |
end; |
623 |
||
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
624 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
625 |
(* Configuration: GUI config, proverinfo messages *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
626 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
627 |
local |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
628 |
val config_file = "~~/lib/ProofGeneral/pgip_isar.xml" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
629 |
val name_attr = pair "name" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
630 |
val version_attr = pair "version" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
631 |
val isabelle_www = "http://isabelle.in.tum.de/" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
632 |
in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
633 |
fun send_pgip_config () = |
16534 | 634 |
let |
635 |
val path = Path.unpack config_file |
|
636 |
val exists = File.exists path |
|
637 |
val proverinfo = |
|
638 |
XML.element "proverinfo" |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
639 |
[("name",Session.name()), ("version", version), |
16534 | 640 |
("url", isabelle_www), ("filenameextns", ".thy;")] |
641 |
[XML.element "welcomemsg" [] [XML.text (Session.welcome())], |
|
642 |
XML.element "helpdoc" |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
643 |
(* NB: would be nice to generate/display docs from isatool |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
644 |
doc, but that program may not be running on same machine; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
645 |
front end should be responsible for launching viewer, etc. *) |
16534 | 646 |
[("name", "Isabelle/HOL Tutorial"), |
647 |
("descr", "A Gentle Introduction to Isabelle/HOL"), |
|
648 |
("url", "http://isabelle.in.tum.de/dist/Isabelle2004/doc/tutorial.pdf")] |
|
649 |
[]] |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
650 |
in |
16534 | 651 |
if exists then |
652 |
(issue_pgips [proverinfo]; issue_pgips [File.read path]) |
|
653 |
else panic ("PGIP configuration file " ^ config_file ^ " not found") |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
654 |
end; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
655 |
end |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
656 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
657 |
|
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
658 |
(* Reveal some information about prover state *) |
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
659 |
fun send_informguise (openfile, opentheory, openproofpos) = |
16534 | 660 |
let val guisefile = |
661 |
case openfile of SOME f => [XML.element "guisefile" |
|
662 |
[("url",Url.pack (Url.File (Path.unpack f)))] []] |
|
663 |
| _ => [] |
|
664 |
val guisetheory = |
|
665 |
case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []] |
|
666 |
| _ => [] |
|
667 |
val guiseproof = |
|
668 |
case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []] |
|
669 |
| _ => [] |
|
670 |
in |
|
671 |
issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)] |
|
672 |
end |
|
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
673 |
|
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
674 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
675 |
(* PGIP identifier tables (prover objects). [incomplete] *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
676 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
677 |
local |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
678 |
val objtype_thy = "theory" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
679 |
val objtype_thm = "theorem" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
680 |
val objtype_term = "term" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
681 |
val objtype_type = "type" |
16534 | 682 |
|
683 |
fun xml_idtable ty ctx ids = |
|
684 |
let |
|
15531 | 685 |
fun ctx_attr (SOME c)= [("context", c)] |
686 |
| ctx_attr NONE = [] |
|
16534 | 687 |
fun xmlid x = XML.element "identifier" [] [XML.text x]; |
688 |
in |
|
689 |
XML.element "idtable" (("objtype", ty)::ctx_attr ctx) |
|
690 |
(map xmlid ids) |
|
691 |
end |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
692 |
in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
693 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
694 |
fun setids t = issue_pgip "setids" [] t |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
695 |
fun addids t = issue_pgip "addids" [] t |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
696 |
fun delids t = issue_pgip "delids" [] t |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
697 |
|
15531 | 698 |
fun delallids ty = setids (xml_idtable ty NONE []) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
699 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
700 |
fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
701 |
fun clear_thy_idtable () = delallids objtype_thy |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
702 |
|
16534 | 703 |
fun send_thm_idtable ctx thy = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
704 |
addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy))); |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
705 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
706 |
fun clear_thm_idtable () = delallids objtype_thm |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
707 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
708 |
(* fun send_type_idtable thy = TODO, it's a bit low-level messy |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
709 |
& maybe not so useful anyway *) |
16534 | 710 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
711 |
end |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
712 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
713 |
(* Response to interface queries about known objects *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
714 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
715 |
local |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
716 |
val topthy = Toplevel.theory_of o Toplevel.get_state |
16486 | 717 |
fun pthm thy name = print_thm (get_thm thy (Name name)) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
718 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
719 |
fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)]) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
720 |
in |
16798 | 721 |
(* FIXME: add askids for "file" here, which returns single theory with same name *) |
15531 | 722 |
fun askids (NONE, SOME "theory") = send_thy_idtable NONE (ThyInfo.names()) |
723 |
| askids (NONE, NONE) = send_thy_idtable NONE (ThyInfo.names()) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
724 |
(* only theories known in top context *) |
15531 | 725 |
| askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy) |
726 |
| askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy) |
|
727 |
| askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy); |
|
16534 | 728 |
send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)) |
15531 | 729 |
| askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.") |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
730 |
|
16534 | 731 |
fun showid (_, "theory", n) = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
732 |
with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n))) |
16534 | 733 |
| showid (SOME thy, "theorem", t) = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
734 |
with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t)) |
16534 | 735 |
| showid (NONE, "theorem", t) = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
736 |
with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
737 |
| showid (_, ot, _) = error ("Cannot show objects of type "^ot) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
738 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
739 |
end |
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
740 |
|
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
741 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
742 |
(** Parsing proof scripts without execution **) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
743 |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
744 |
(* Notes. |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
745 |
This is quite tricky, because 1) we need to put back whitespace which |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
746 |
was removed during parsing so we can provide markup around commands; |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
747 |
2) parsing is intertwined with execution in Isar so we have to repeat |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
748 |
the parsing to extract interesting parts of commands. The trace of |
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
749 |
tokens parsed which is now recorded in each transition (added by |
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
750 |
Markus June '04) helps do this, but the mechanism is still a bad mess. |
16534 | 751 |
|
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
752 |
If we had proper parse trees it would be easy, although having a |
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
753 |
fixed type of trees might be tricky with Isar's extensible parser. |
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
754 |
|
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
755 |
Probably the best solution is to produce the meta-information at |
16534 | 756 |
the same time as the parse, for each command, e.g. by recording a |
757 |
list of (name,objtype) pairs which record the bindings created by |
|
758 |
a command. This would require changing the interfaces in |
|
759 |
outer_syntax.ML (or providing new ones), |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
760 |
|
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
761 |
datatype metainfo = Binding of string * string (* name, objtype *) |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
762 |
|
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
763 |
val command_withmetainfo: string -> string -> string -> |
16534 | 764 |
(token list -> |
765 |
((Toplevel.transition -> Toplevel.transition) * metainfo list) * |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
766 |
token list) -> parser |
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
767 |
|
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
768 |
We'd also like to render terms as they appear in output, but this |
16534 | 769 |
will be difficult because inner syntax is extensible and we don't |
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
770 |
have the correct syntax to hand when just doing outer parsing |
16534 | 771 |
without execution. A reasonable approximation could |
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
772 |
perhaps be obtained by using the syntax of the current context. |
16534 | 773 |
However, this would mean more mess trying to pick out terms, |
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
774 |
so at this stage a more serious change to the Isar functions |
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
775 |
seems necessary. |
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
776 |
*) |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
777 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
778 |
local |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
779 |
fun markup_text str elt = [XML.element elt [] [XML.text str]] |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
780 |
fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]] |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
781 |
fun empty elt = [XML.element elt [] []] |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
782 |
|
15210
4ff917a91e16
Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
aspinall
parents:
15208
diff
changeset
|
783 |
fun whitespace str = XML.element "whitespace" [] [XML.text str] |
15208
09271a87fbf0
Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
aspinall
parents:
15192
diff
changeset
|
784 |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
785 |
(* an extra token is needed to terminate the command *) |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
786 |
val sync = OuterSyntax.scan "\\<^sync>"; |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
787 |
|
16534 | 788 |
fun named_item_elt_with nameattr toks str elt nameP objtyp = |
789 |
let |
|
790 |
val name = (fst (nameP (toks@sync))) |
|
791 |
handle _ => (error ("Error occurred in name parser for " ^ elt ^ |
|
792 |
"(objtype: " ^ objtyp ^ ")"); |
|
793 |
"") |
|
794 |
||
795 |
in |
|
796 |
[XML.element elt |
|
797 |
((if name="" then [] else [(nameattr, name)])@ |
|
798 |
(if objtyp="" then [] else [("objtype", objtyp)])) |
|
799 |
([XML.text str])] |
|
800 |
end |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
801 |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
802 |
val named_item_elt = named_item_elt_with "name" |
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
803 |
val thmnamed_item_elt = named_item_elt_with "thmname" |
16534 | 804 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
805 |
fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
806 |
|
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
807 |
(* FIXME: allow dynamic extensions to language here: we need a hook in |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
808 |
outer_syntax.ML to reset this table. *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
809 |
|
16534 | 810 |
val keywords_classification_table = ref (NONE: string Symtab.table option) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
811 |
|
16534 | 812 |
fun get_keywords_classification_table () = |
813 |
case (!keywords_classification_table) of |
|
814 |
SOME t => t |
|
815 |
| NONE => (let |
|
816 |
val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) |
|
817 |
(Symtab.empty,OuterSyntax.dest_parsers()) |
|
818 |
in (keywords_classification_table := SOME tab; tab) end) |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
819 |
|
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
820 |
|
16534 | 821 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
822 |
fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *) |
16534 | 823 |
let |
824 |
val ((thyname,imports,files),_) = ThyHeader.args (toks@sync) |
|
825 |
in |
|
826 |
markup_text_attrs str "opentheory" |
|
827 |
([("thyname",thyname)] @ |
|
828 |
(if imports=[] then [] else |
|
829 |
[("parentnames", (space_implode ";" imports) ^ ";")])) |
|
830 |
end |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
831 |
|
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
832 |
fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *) |
16534 | 833 |
let |
834 |
(* NB: PGIP only deals with single name bindings at the moment; |
|
835 |
potentially we could markup grouped definitions several times but |
|
836 |
that might suggest the wrong structure to the editor? |
|
837 |
Better alternative would be to put naming closer around text, |
|
838 |
but to do that we'd be much better off modifying the real parser |
|
839 |
instead of reconstructing it here. *) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
840 |
|
16534 | 841 |
val plain_items = (* no names, unimportant names, or too difficult *) |
842 |
["defaultsort","arities","judgement","finalconsts", |
|
843 |
"syntax", "nonterminals", "translations", |
|
844 |
"global", "local", "hide", |
|
845 |
"ML_setup", "setup", "method_setup", |
|
846 |
"parse_ast_translation", "parse_translation", "print_translation", |
|
847 |
"typed_print_translation", "print_ast_translation", "token_translation", |
|
848 |
"oracle", |
|
849 |
"declare"] |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
850 |
|
16534 | 851 |
val plain_item = markup_text str "theoryitem" |
852 |
val comment_item = markup_text str "litcomment" |
|
853 |
val named_item = named_item_elt toks str "theoryitem" |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
854 |
|
16534 | 855 |
val opt_overloaded = P.opt_keyword "overloaded"; |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
856 |
|
16534 | 857 |
val thmnameP = (* see isar_syn.ML/theoremsP *) |
858 |
let |
|
859 |
val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1) |
|
16958 | 860 |
val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x) |
16534 | 861 |
in |
862 |
theoremsP |
|
863 |
end |
|
864 |
in |
|
865 |
(* TODO: ideally we would like to render terms properly, just as they are |
|
866 |
in output. This implies using PGML for symbols and variables/atoms. |
|
867 |
BUT it's rather tricky without having the correct concrete syntax to hand, |
|
868 |
and even if we did, we'd have to mess around here a whole lot more first |
|
869 |
to pick out the terms from the syntax. *) |
|
15254
10cfd6a14682
Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents:
15253
diff
changeset
|
870 |
|
16534 | 871 |
if (name mem plain_items) then plain_item |
872 |
else case name of |
|
873 |
"text" => comment_item |
|
874 |
| "text_raw" => comment_item |
|
875 |
| "typedecl" => named_item (P.type_args |-- P.name) "type" |
|
876 |
| "types" => named_item (P.type_args |-- P.name) "type" |
|
877 |
| "classes" => named_item P.name "class" |
|
878 |
| "classrel" => named_item P.name "class" |
|
879 |
| "consts" => named_item (P.const >> #1) "term" |
|
880 |
| "axioms" => named_item (P.spec_name >> (#1 o #1)) "theorem" |
|
881 |
| "defs" => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem" |
|
882 |
| "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term" |
|
883 |
| "theorems" => named_item thmnameP "thmset" |
|
884 |
| "lemmas" => named_item thmnameP "thmset" |
|
885 |
| "oracle" => named_item P.name "oracle" |
|
886 |
| "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale" |
|
887 |
| _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item) |
|
888 |
end |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
889 |
|
16534 | 890 |
fun xmls_of_thy_goal (name,toks,str) = |
891 |
let |
|
892 |
(* see isar_syn.ML/gen_theorem *) |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
893 |
val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); |
16534 | 894 |
val general_statement = |
895 |
statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement); |
|
896 |
||
897 |
val gen_theoremP = |
|
16958 | 898 |
P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --| |
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
899 |
Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) -- |
16534 | 900 |
general_statement >> (fn ((locale, a), (elems, concl)) => |
901 |
fst a) (* a : (bstring * Args.src list) *) |
|
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
902 |
|
16958 | 903 |
val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "") |
16534 | 904 |
(* TODO: add preference values for attributes |
905 |
val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)] |
|
906 |
*) |
|
907 |
in |
|
908 |
(thmnamed_item_elt toks str "opengoal" nameP "") @ |
|
909 |
(empty "openblock") |
|
910 |
end |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
911 |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
912 |
fun xmls_of_qed (name,markup) = |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
913 |
let val qedmarkup = |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
914 |
(case name of |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
915 |
"sorry" => markup "postponegoal" |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
916 |
| "oops" => markup "giveupgoal" |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
917 |
| "done" => markup "closegoal" |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
918 |
| "by" => markup "closegoal" (* nested or toplevel *) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
919 |
| "qed" => markup "closegoal" (* nested or toplevel *) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
920 |
| "." => markup "closegoal" (* nested or toplevel *) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
921 |
| ".." => markup "closegoal" (* nested or toplevel *) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
922 |
| other => (* default to closegoal: may be wrong for extns *) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
923 |
(parse_warning |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
924 |
("Unrecognized qed command: " ^ quote other); |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
925 |
markup "closegoal")) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
926 |
in qedmarkup @ (empty "closeblock") end |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
927 |
|
16534 | 928 |
fun xmls_of_kind kind (name,toks,str) = |
929 |
let val markup = markup_text str in |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
930 |
case kind of |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
931 |
"control" => markup "badcmd" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
932 |
| "diag" => markup "spuriouscmd" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
933 |
(* theory/files *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
934 |
| "theory-begin" => xmls_of_thy_begin (name,toks,str) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
935 |
| "theory-decl" => xmls_of_thy_decl (name,toks,str) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
936 |
| "theory-heading" => markup "litcomment" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
937 |
| "theory-script" => markup "theorystep" |
15146
eab7de0d0a31
Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents:
15145
diff
changeset
|
938 |
| "theory-end" => markup "closetheory" |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
939 |
(* proof control *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
940 |
| "theory-goal" => xmls_of_thy_goal (name,toks,str) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
941 |
| "proof-heading" => markup "litcomment" |
15225
68ab0f4eb457
Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents:
15220
diff
changeset
|
942 |
| "proof-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: have, show, ... *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
943 |
| "proof-block" => markup "proofstep" (* context-shift: proof, next; really "newgoal" *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
944 |
| "proof-open" => (empty "openblock") @ (markup "proofstep") |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
945 |
| "proof-close" => (markup "proofstep") @ (empty "closeblock") |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
946 |
| "proof-script" => markup "proofstep" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
947 |
| "proof-chain" => markup "proofstep" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
948 |
| "proof-decl" => markup "proofstep" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
949 |
| "proof-asm" => markup "proofstep" |
15289 | 950 |
| "proof-asm-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: obtain *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
951 |
| "qed" => xmls_of_qed (name,markup) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
952 |
| "qed-block" => xmls_of_qed (name,markup) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
953 |
| "qed-global" => xmls_of_qed (name,markup) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
954 |
| other => (* default for anything else is "spuriouscmd", ignored for undo. *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
955 |
(parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other); |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
956 |
markup "spuriouscmd") |
16534 | 957 |
end |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
958 |
in |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
959 |
|
16534 | 960 |
fun xmls_of_transition (name,str,toks) = |
961 |
let |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
962 |
val classification = Symtab.lookup (get_keywords_classification_table(),name) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
963 |
in case classification of |
16534 | 964 |
SOME k => (xmls_of_kind k (name,toks,str)) |
965 |
| NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *) |
|
966 |
(parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd"); |
|
967 |
markup_text str "spuriouscmd") |
|
968 |
end |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
969 |
|
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
970 |
fun markup_toks [] _ = [] |
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
971 |
| markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x |
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
972 |
|
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
973 |
fun markup_comment_whs [] = [] |
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
974 |
| markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *) |
16534 | 975 |
let |
976 |
val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks |
|
977 |
in |
|
978 |
if (prewhs <> []) then |
|
979 |
whitespace (implode (map OuterLex.unparse prewhs)) |
|
980 |
:: (markup_comment_whs rest) |
|
981 |
else |
|
982 |
(markup_text (OuterLex.unparse t) "comment") @ |
|
983 |
(markup_comment_whs ts) |
|
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
984 |
end |
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
985 |
|
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
986 |
fun xmls_pre_cmd [] = ([],[]) |
16534 | 987 |
| xmls_pre_cmd toks = |
988 |
let |
|
989 |
(* an extra token is needed to terminate the command *) |
|
990 |
val sync = OuterSyntax.scan "\\<^sync>"; |
|
991 |
val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode |
|
992 |
val text_with_whs = |
|
993 |
((spaceP || Scan.succeed "") -- |
|
994 |
(P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^) |
|
995 |
-- (spaceP || Scan.succeed "") >> op^ |
|
996 |
val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync) |
|
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
997 |
(* NB: this collapses litcomment,(litcomment|whitespace)* to a single litcomment *) |
16534 | 998 |
val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1 |
999 |
val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1000 |
in |
16534 | 1001 |
((markup_comment_whs prewhs) @ |
1002 |
(if (length rest2 = length rest1) then [] |
|
1003 |
else markup_text (implode |
|
1004 |
(map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))) |
|
1005 |
"litcomment") @ |
|
1006 |
(markup_comment_whs postwhs), |
|
1007 |
Library.take (length rest3 - 1,rest3)) |
|
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
1008 |
end |
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
1009 |
|
16534 | 1010 |
fun xmls_of_impropers toks = |
1011 |
let |
|
1012 |
val (xmls,rest) = xmls_pre_cmd toks |
|
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
1013 |
in |
16534 | 1014 |
xmls @ (markup_toks rest "unparseable") |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1015 |
end |
16534 | 1016 |
|
1017 |
fun markup_unparseable str = markup_text str "unparseable" |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1018 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1019 |
end |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1020 |
|
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1021 |
|
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1022 |
local |
16534 | 1023 |
(* we have to weave together the whitespace/comments with proper tokens |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1024 |
to reconstruct the input. *) |
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
1025 |
(* TODO: see if duplicating isar_output/parse_thy can help here *) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1026 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1027 |
fun match_tokens ([],us,vs) = (rev vs,us) (* used, unused *) |
16534 | 1028 |
| match_tokens (t::ts,w::ws,vs) = |
1029 |
if (t = w) then match_tokens (ts,ws,w::vs) |
|
1030 |
else match_tokens (t::ts,ws,w::vs) |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1031 |
| match_tokens _ = error ("match_tokens: mismatched input parse") |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1032 |
in |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1033 |
fun xmls_of_str str = |
16534 | 1034 |
let |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1035 |
(* parsing: See outer_syntax.ML/toplevel_source *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1036 |
fun parse_loop ([],[],xmls) = xmls |
16534 | 1037 |
| parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks) |
1038 |
| parse_loop ((nm,toks,_)::trs,itoks,xmls) = |
|
1039 |
let |
|
1040 |
(* first proper token after whitespace/litcomment/whitespace is command *) |
|
1041 |
val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks |
|
1042 |
val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs) |
|
1043 |
| _ => error("proof_general/parse_loop impossible") |
|
1044 |
val (utoks,itoks'') = match_tokens (toks,itoks',[]) |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1045 |
(* FIXME: should take trailing [w/s+] semicolon too in utoks *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1046 |
|
16534 | 1047 |
val str = implode (map OuterLex.unparse (cmdtok::utoks)) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1048 |
|
16534 | 1049 |
val xmls_tr = xmls_of_transition (nm,str,toks) |
1050 |
in |
|
1051 |
parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr) |
|
1052 |
end |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1053 |
in |
16534 | 1054 |
(let val toks = OuterSyntax.scan str |
1055 |
in |
|
1056 |
parse_loop (OuterSyntax.read toks, toks, []) |
|
1057 |
end) |
|
1058 |
handle _ => markup_unparseable str |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1059 |
end |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1060 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1061 |
|
16534 | 1062 |
fun parsescript str attrs = |
1063 |
let |
|
1064 |
val _ = start_delay_msgs () (* accumulate error messages to put inside parseresult *) |
|
1065 |
val xmls = xmls_of_str str |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1066 |
val errs = end_delayed_msgs () |
16534 | 1067 |
in |
1068 |
issue_pgips [XML.element "parseresult" attrs (errs@xmls)] |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1069 |
end |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1070 |
end |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1071 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1072 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1073 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1074 |
(**** PGIP: Isabelle -> Interface ****) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1075 |
|
16534 | 1076 |
val isabelle_pgml_version_supported = "1.0"; |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1077 |
val isabelle_pgip_version_supported = "2.0" |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1078 |
|
16798 | 1079 |
(* TODO: would be cleaner to define a datatype here for the accepted elements, |
1080 |
and mapping functions to/from strings. At the moment this list must |
|
1081 |
coincide with the strings in the function process_pgip_element. *) |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1082 |
val isabelle_acceptedpgipelems = |
16798 | 1083 |
["askpgip","askpgml","askprefs","getpref","setpref", |
1084 |
"proverinit","proverexit","startquiet","stopquiet", |
|
1085 |
"pgmlsymbolson", "pgmlsymbolsoff", |
|
1086 |
"dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal", |
|
1087 |
"askids", "showid", "askguise", |
|
1088 |
"parsescript", |
|
1089 |
"showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc", |
|
1090 |
"doitem", "undoitem", "redoitem", "abortheory", |
|
1091 |
"retracttheory", "loadfile", "openfile", "closefile", |
|
1092 |
"abortfile", "changecwd", "systemcmd"]; |
|
1093 |
||
16534 | 1094 |
fun usespgip () = |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1095 |
issue_pgip |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1096 |
"usespgip" |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1097 |
[("version", isabelle_pgip_version_supported)] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1098 |
(XML.element "acceptedpgipelems" [] |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1099 |
(map (fn s=>XML.element "pgipelem" |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1100 |
[] (* if threads: possibility to add async here *) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1101 |
[s]) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1102 |
isabelle_acceptedpgipelems)) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1103 |
|
16534 | 1104 |
fun usespgml () = |
16798 | 1105 |
issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)] |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1106 |
|
16534 | 1107 |
fun hasprefs () = |
15570 | 1108 |
List.app (fn (prefcat, prefs) => |
16534 | 1109 |
issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)] |
1110 |
(map (fn (name, (descr, (ty, (default,_),_))) => |
|
1111 |
XML.element "haspref" [("name", name), |
|
1112 |
("descr", descr), |
|
1113 |
("default", default)] |
|
16798 | 1114 |
[ty]) prefs)]) (!preferences) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1115 |
|
15570 | 1116 |
fun allprefs () = Library.foldl (op @) ([], map snd (!preferences)) |
16534 | 1117 |
|
1118 |
fun setpref name value = |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1119 |
(case assoc (allprefs(), name) of |
16534 | 1120 |
NONE => warning ("Unknown pref: " ^ quote name) |
15531 | 1121 |
| SOME (_, (_, _, set)) => set value); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1122 |
|
16534 | 1123 |
fun getpref name = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1124 |
(case assoc (allprefs(), name) of |
16534 | 1125 |
NONE => warning ("Unknown pref: " ^ quote name) |
1126 |
| SOME (_, (_, (_,get), _)) => |
|
1127 |
issue_pgip "prefval" [("name", name)] (get ())); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1128 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1129 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1130 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1131 |
(**** PGIP: Interface -> Isabelle/Isar ****) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1132 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1133 |
exception PGIP of string; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1134 |
exception PGIP_QUIT; |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1135 |
|
16534 | 1136 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1137 |
(* Sending commands to Isar *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1138 |
|
16534 | 1139 |
fun isarcmd s = |
1140 |
s |> OuterSyntax.scan |> OuterSyntax.read |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1141 |
|> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>; |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1142 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1143 |
fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1144 |
| xmltext [] = "" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1145 |
| xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)" |
16534 | 1146 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1147 |
fun isarscript xmls = isarcmd (xmltext xmls) (* send a script command *) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1148 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1149 |
|
16791 | 1150 |
(* load an arbitrary file (must be .thy or .ML) *) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1151 |
|
16534 | 1152 |
fun use_thy_or_ml_file file = |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1153 |
let |
16534 | 1154 |
val (path,extn) = Path.split_ext (Path.unpack file) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1155 |
in |
16534 | 1156 |
case extn of |
1157 |
"" => isarcmd ("use_thy " ^ (quote (Path.pack path))) |
|
1158 |
| "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path))) |
|
1159 |
| "ML" => isarcmd ("use " ^ quote file) |
|
1160 |
| other => error ("Don't know how to read a file with extension " ^ other) |
|
1161 |
end |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1162 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1163 |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1164 |
(* Proof control commands *) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1165 |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1166 |
local |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1167 |
fun xmlattro attr attrs = assoc(attrs,attr) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1168 |
|
16534 | 1169 |
fun xmlattr attr attrs = |
1170 |
(case xmlattro attr attrs of |
|
1171 |
SOME value => value |
|
1172 |
| NONE => raise PGIP ("Missing attribute: " ^ attr)) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1173 |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1174 |
val thyname_attro = xmlattro "thyname" |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1175 |
val thyname_attr = xmlattr "thyname" |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1176 |
val objtype_attro = xmlattro "objtype" |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1177 |
val objtype_attr = xmlattr "objtype" |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1178 |
val name_attr = xmlattr "name" |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1179 |
val dirname_attr = xmlattr "dir" |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1180 |
fun comment x = "(* " ^ x ^ " *)" |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1181 |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1182 |
fun localfile_of_url url = (* only handle file:/// or file://localhost/ *) |
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1183 |
case Url.unpack url of |
16534 | 1184 |
(Url.File path) => File.platform_path path |
1185 |
| _ => error ("Cannot access non-local URL " ^ url) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1186 |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1187 |
val fileurl_of = localfile_of_url o (xmlattr "url") |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1188 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1189 |
val topthy = Toplevel.theory_of o Toplevel.get_state |
16440 | 1190 |
val topthy_name = Context.theory_name o topthy |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1191 |
|
15531 | 1192 |
val currently_open_file = ref (NONE : string option) |
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
1193 |
|
16791 | 1194 |
(* Path management: we allow theory files to have dependencies |
1195 |
in their own directory, but when we change directory for a new |
|
1196 |
file we remove the path. Leaving it there can cause confusion |
|
1197 |
with difference in batch mode.a NB: PGIP does not assume |
|
1198 |
that the prover has a load path. *) |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1199 |
local |
16791 | 1200 |
val current_working_dir = ref (NONE : string option) |
1201 |
in |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1202 |
fun changecwd dir = |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1203 |
(case (!current_working_dir) of |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1204 |
NONE => () |
16791 | 1205 |
| SOME dir => ThyLoad.del_path dir; |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1206 |
ThyLoad.add_path dir; |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1207 |
current_working_dir := SOME dir) |
16791 | 1208 |
end |
1209 |
||
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
1210 |
val topnode = Toplevel.node_of o Toplevel.get_state |
16534 | 1211 |
fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph) |
1212 |
| _ => NONE) handle Toplevel.UNDEF => NONE |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1213 |
in |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1214 |
|
16534 | 1215 |
fun process_pgip_element pgipxml = (case pgipxml of |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1216 |
(XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t) |
16534 | 1217 |
| (xml as (XML.Elem (elem, attrs, data))) => |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1218 |
(case elem of |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1219 |
(* protocol config *) |
16534 | 1220 |
"askpgip" => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *) |
1221 |
usespgip (); send_pgip_config ()) |
|
1222 |
| "askpgml" => usespgml () |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1223 |
(* proverconfig *) |
16534 | 1224 |
| "askprefs" => hasprefs () |
1225 |
| "getpref" => getpref (name_attr attrs) |
|
1226 |
| "setpref" => setpref (name_attr attrs) (xmltext data) |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1227 |
(* provercontrol *) |
16534 | 1228 |
| "proverinit" => isar_restart () |
1229 |
| "proverexit" => isarcmd "quit" |
|
1230 |
| "startquiet" => isarcmd "disable_pr" |
|
1231 |
| "stopquiet" => isarcmd "enable_pr" |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1232 |
| "pgmlsymbolson" => change print_mode (insert (op =) Symbol.xsymbolsN) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1233 |
| "pgmlsymbolsoff" => change print_mode (remove (op =) Symbol.xsymbolsN) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1234 |
(* properproofcmd: proper commands which belong in script *) |
15401
ba28d103bada
Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents:
15400
diff
changeset
|
1235 |
(* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *) |
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
1236 |
(* NB: Isar doesn't make lemma name of goal accessible during proof *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1237 |
| "opengoal" => isarscript data |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1238 |
| "proofstep" => isarscript data |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1239 |
| "closegoal" => isarscript data |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1240 |
| "giveupgoal" => isarscript data |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1241 |
| "postponegoal" => isarscript data |
16534 | 1242 |
| "comment" => isarscript data (* NB: should be ignored, but process anyway *) |
1243 |
| "whitespace" => isarscript data (* NB: should be ignored, but process anyway *) |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1244 |
| "litcomment" => isarscript data |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1245 |
| "spuriouscmd" => isarscript data |
16534 | 1246 |
| "badcmd" => isarscript data |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1247 |
(* improperproofcmd: improper commands which *do not* belong in script *) |
15401
ba28d103bada
Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents:
15400
diff
changeset
|
1248 |
| "dostep" => isarscript data |
15286 | 1249 |
| "undostep" => isarcmd "undos_proof 1" |
15626 | 1250 |
| "redostep" => isarcmd "redo" |
16534 | 1251 |
| "abortgoal" => isarcmd "ProofGeneral.kill_proof" |
1252 |
| "forget" => error "Not implemented" |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1253 |
| "restoregoal" => error "Not implemented" (* could just treat as forget? *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1254 |
(* proofctxt: improper commands *) |
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1255 |
| "askids" => askids (thyname_attro attrs, objtype_attro attrs) |
16534 | 1256 |
| "showid" => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs) |
1257 |
| "askguise" => send_informguise (!currently_open_file, |
|
1258 |
SOME (topthy_name()) handle Toplevel.UNDEF => NONE, |
|
1259 |
topproofpos()) |
|
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1260 |
| "parsescript" => parsescript (xmltext data) attrs (* just pass back attrs unchanged *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1261 |
| "showproofstate" => isarcmd "pr" |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1262 |
| "showctxt" => isarcmd "print_theory" (* more useful than print_context *) |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1263 |
| "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1264 |
| "setlinewidth" => isarcmd ("pretty_setmargin " ^ xmltext data) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1265 |
| "viewdoc" => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1266 |
(* properfilecmd: proper theory-level script commands *) |
15401
ba28d103bada
Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents:
15400
diff
changeset
|
1267 |
(* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1268 |
| "opentheory" => isarscript data |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1269 |
| "theoryitem" => isarscript data |
16534 | 1270 |
| "closetheory" => let |
1271 |
val thyname = topthy_name() |
|
1272 |
in (isarscript data; |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1273 |
writeln ("Theory " ^ quote thyname ^ " completed.")) |
16534 | 1274 |
end |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1275 |
(* improperfilecmd: theory-level commands not in script *) |
15401
ba28d103bada
Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents:
15400
diff
changeset
|
1276 |
| "doitem" => isarscript data |
15286 | 1277 |
| "undoitem" => isarcmd "ProofGeneral.undo" |
15626 | 1278 |
| "redoitem" => isarcmd "ProofGeneral.redo" |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1279 |
| "aborttheory" => isarcmd ("init_toplevel") |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1280 |
| "retracttheory" => isarcmd ("kill_thy " ^ quote (thyname_attr attrs)) |
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1281 |
| "loadfile" => use_thy_or_ml_file (fileurl_of attrs) |
15629
4066f01f1beb
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents:
15626
diff
changeset
|
1282 |
| "openfile" => (openfile_retract (fileurl_of attrs); |
16534 | 1283 |
currently_open_file := SOME (fileurl_of attrs)) |
1284 |
| "closefile" => (case !currently_open_file of |
|
1285 |
SOME f => (inform_file_processed f; |
|
1286 |
currently_open_file := NONE) |
|
1287 |
| NONE => raise PGIP ("closefile when no file is open!")) |
|
15531 | 1288 |
| "abortfile" => (currently_open_file := NONE) (* perhaps error for no file open *) |
16791 | 1289 |
| "changecwd" => changecwd (dirname_attr attrs) |
16534 | 1290 |
| "systemcmd" => isarscript data |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1291 |
(* unofficial command for debugging *) |
16534 | 1292 |
| "quitpgip" => raise PGIP_QUIT |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1293 |
| _ => raise PGIP ("Unrecognized PGIP element: " ^ elem))) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1294 |
|
16534 | 1295 |
fun process_pgip_tree xml = |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1296 |
(pgip_refid := NONE; |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1297 |
pgip_refseq := NONE; |
15173
e1582a0d29b5
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents:
15156
diff
changeset
|
1298 |
(case xml of |
16534 | 1299 |
XML.Elem ("pgip", attrs, pgips) => |
1300 |
(let |
|
1301 |
val class = xmlattr "class" attrs |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1302 |
val dest = xmlattro "destid" attrs |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1303 |
val _ = (pgip_refid := xmlattro "id" attrs; |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1304 |
pgip_refseq := xmlattro "seq" attrs) |
16534 | 1305 |
in |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1306 |
(* We respond to broadcast messages to provers, or |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1307 |
messages intended uniquely for us. Silently ignore rest. *) |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1308 |
case dest of |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1309 |
NONE => if (class = "pa") then |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1310 |
(List.app process_pgip_element pgips; true) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1311 |
else false |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1312 |
| SOME id => if (matching_pgip_id id) then |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1313 |
(List.app process_pgip_element pgips; true) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1314 |
else false |
16534 | 1315 |
end) |
1316 |
| _ => raise PGIP "Invalid PGIP packet received") |
|
1317 |
handle (PGIP msg) => |
|
1318 |
(error (msg ^ "\nPGIP error occured in XML text below:\n" ^ |
|
1319 |
(XML.string_of_tree xml)))) |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1320 |
|
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1321 |
val process_pgip = K () o process_pgip_tree o XML.tree_of_string |
15191
5ca1fd9dec83
Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents:
15173
diff
changeset
|
1322 |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1323 |
end |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1324 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1325 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1326 |
(* PGIP loop: process PGIP input only *) |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1327 |
|
16534 | 1328 |
local |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1329 |
|
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1330 |
exception XML_PARSE |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1331 |
|
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1332 |
fun loop ready src = |
16534 | 1333 |
let |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1334 |
val _ = if ready then (issue_pgipe "ready" []) else () |
16534 | 1335 |
val pgipo = (Source.get_single src) |
1336 |
handle e => raise XML_PARSE |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1337 |
in |
16534 | 1338 |
case pgipo of |
1339 |
NONE => () |
|
1340 |
| SOME (pgip,src') => |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1341 |
let |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1342 |
val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true) |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1343 |
in |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1344 |
loop ready' src' |
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1345 |
end |
15531 | 1346 |
end handle e => handler (e,SOME src) (* i.e. error in ready/XML parse *) |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1347 |
|
16534 | 1348 |
and handler (e,srco) = |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1349 |
case (e,srco) of |
16534 | 1350 |
(XML_PARSE,SOME src) => |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1351 |
panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1352 |
| (PGIP_QUIT,_) => () |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1353 |
| (ERROR,SOME src) => loop true src (* message already given *) |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1354 |
| (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src) |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1355 |
| (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *) |
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1356 |
| (e,SOME src) => (error (Toplevel.exn_message e); loop true src) |
15531 | 1357 |
| (_,NONE) => () |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1358 |
in |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1359 |
(* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *) |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1360 |
|
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1361 |
val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single |
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1362 |
|
15531 | 1363 |
val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty) |
15145
07360eef9f4f
Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents:
15134
diff
changeset
|
1364 |
|
16824 | 1365 |
fun pgip_toplevel x = loop true x |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1366 |
end |
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1367 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1368 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1369 |
(* additional outer syntax for Isar *) |
12778 | 1370 |
|
17057 | 1371 |
local structure P = OuterParse and K = OuterKeyword in |
12778 | 1372 |
|
16534 | 1373 |
val undoP = (*undo without output*) |
12778 | 1374 |
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control |
1375 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); |
|
1376 |
||
16534 | 1377 |
val redoP = (*redo without output*) |
15626 | 1378 |
OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control |
1379 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.redo)); |
|
1380 |
||
12778 | 1381 |
val context_thy_onlyP = |
1382 |
OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control |
|
1383 |
(P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only)); |
|
1384 |
||
1385 |
val try_context_thy_onlyP = |
|
1386 |
OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control |
|
1387 |
(P.name >> (Toplevel.no_timing oo |
|
1388 |
(Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only))); |
|
1389 |
||
1390 |
val restartP = |
|
1391 |
OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control |
|
1392 |
(P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart))); |
|
1393 |
||
1394 |
val kill_proofP = |
|
1395 |
OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control |
|
1396 |
(Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); |
|
1397 |
||
1398 |
val inform_file_processedP = |
|
1399 |
OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control |
|
14902
bef0dc694c48
Path.split_ext; more robust inform_file_processed;
wenzelm
parents:
14880
diff
changeset
|
1400 |
(P.name >> (fn file => Toplevel.no_timing o |
bef0dc694c48
Path.split_ext; more robust inform_file_processed;
wenzelm
parents:
14880
diff
changeset
|
1401 |
Toplevel.keep (vacuous_inform_file_processed file) o |
bef0dc694c48
Path.split_ext; more robust inform_file_processed;
wenzelm
parents:
14880
diff
changeset
|
1402 |
Toplevel.kill o |
bef0dc694c48
Path.split_ext; more robust inform_file_processed;
wenzelm
parents:
14880
diff
changeset
|
1403 |
Toplevel.keep (proper_inform_file_processed file))); |
12778 | 1404 |
|
1405 |
val inform_file_retractedP = |
|
1406 |
OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control |
|
1407 |
(P.name >> (Toplevel.no_timing oo |
|
14902
bef0dc694c48
Path.split_ext; more robust inform_file_processed;
wenzelm
parents:
14880
diff
changeset
|
1408 |
(fn file => Toplevel.imperative (fn () => inform_file_retracted file)))); |
12778 | 1409 |
|
14725 | 1410 |
val process_pgipP = |
1411 |
OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control |
|
1412 |
(P.text >> (Toplevel.no_timing oo |
|
1413 |
(fn txt => Toplevel.imperative (fn () => process_pgip txt)))); |
|
1414 |
||
12778 | 1415 |
fun init_outer_syntax () = OuterSyntax.add_parsers |
15626 | 1416 |
[undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP, |
14725 | 1417 |
inform_file_processedP, inform_file_retractedP, process_pgipP]; |
12778 | 1418 |
|
1419 |
end; |
|
1420 |
||
1421 |
||
1422 |
(* init *) |
|
1423 |
||
1424 |
val initialized = ref false; |
|
1425 |
||
16534 | 1426 |
fun set_prompts true _ = ml_prompts "ML> " "ML# " |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1427 |
| set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# " |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1428 |
| set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "373"); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1429 |
|
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1430 |
fun init_setup isar pgip = |
16534 | 1431 |
(conditional (not (! initialized)) (fn () => |
12778 | 1432 |
(if isar then setmp warning_fn (K ()) init_outer_syntax () else (); |
1433 |
setup_xsymbols_output (); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1434 |
setup_pgml_output (); |
12778 | 1435 |
setup_messages (); |
1436 |
setup_state (); |
|
1437 |
setup_thy_loader (); |
|
13526 | 1438 |
setup_present_hook (); |
12778 | 1439 |
set initialized; ())); |
1440 |
sync_thy_loader (); |
|
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1441 |
change print_mode (cons proof_generalN o remove (op =) proof_generalN); |
16534 | 1442 |
if pgip then |
16821
ba1f6aba44ed
Update PGIP packet handling, fixing unique session identifier.
aspinall
parents:
16816
diff
changeset
|
1443 |
(init_pgip_session_id(); |
17217
954c0f265203
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents:
17057
diff
changeset
|
1444 |
change print_mode (append [pgmlN, pgmlatomsN] o fold (remove (op =)) [pgmlN, pgmlatomsN])) |
16534 | 1445 |
else |
1446 |
pgip_emacs_compatibility_flag := true; (* assume this for PG <3.6 compatibility *) |
|
12778 | 1447 |
set quick_and_dirty; |
1448 |
ThmDeps.enable (); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1449 |
set_prompts isar pgip; |
16534 | 1450 |
pgip_active := pgip); |
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1451 |
|
16534 | 1452 |
fun init isar = |
1453 |
(init_setup isar false; |
|
1454 |
if isar then Isar.sync_main () else isa_restart ()); |
|
15134
d3fa5e1d6e4d
Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents:
15010
diff
changeset
|
1455 |
|
16534 | 1456 |
fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode." |
1457 |
| init_pgip true = (init_setup true true; pgip_toplevel tty_src); |
|
12778 | 1458 |
|
1459 |
||
1460 |
||
16534 | 1461 |
(** generate elisp file for keyword classification **) |
12778 | 1462 |
|
1463 |
local |
|
1464 |
||
1465 |
val regexp_meta = explode ".*+?[]^$"; |
|
16534 | 1466 |
val regexp_quote = |
1467 |
implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode; |
|
12778 | 1468 |
|
1469 |
fun defconst name strs = |
|
1470 |
"\n(defconst isar-keywords-" ^ name ^ |
|
1471 |
"\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; |
|
1472 |
||
16534 | 1473 |
fun make_elisp_commands commands kind = defconst kind |
1474 |
(commands |> List.mapPartial (fn (c, _, k, _) => if k = kind then SOME c else NONE)); |
|
12778 | 1475 |
|
1476 |
fun make_elisp_syntax (keywords, commands) = |
|
1477 |
";;\n\ |
|
1478 |
\;; Keyword classification tables for Isabelle/Isar.\n\ |
|
1479 |
\;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\ |
|
1480 |
\;;\n\ |
|
1481 |
\;; $" ^ "Id$\n\ |
|
1482 |
\;;\n" ^ |
|
1483 |
defconst "major" (map #1 commands) ^ |
|
15570 | 1484 |
defconst "minor" (List.filter Syntax.is_identifier keywords) ^ |
17057 | 1485 |
implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^ |
12778 | 1486 |
"\n(provide 'isar-keywords)\n"; |
1487 |
||
1488 |
in |
|
1489 |
||
1490 |
fun write_keywords s = |
|
16534 | 1491 |
(init_outer_syntax (); |
1492 |
File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el")) |
|
1493 |
(make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()))); |
|
12778 | 1494 |
|
1495 |
end; |
|
1496 |
||
16534 | 1497 |
end; |