author | wenzelm |
Mon, 13 May 2013 21:03:30 +0200 | |
changeset 51967 | 43fbd02eb9d0 |
parent 51965 | 4af6884329cb |
child 51969 | 1767d4feef7d |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/proof_general_pgip.ML |
2 |
Author: David Aspinall and Markus Wenzel |
|
3 |
||
4 |
Isabelle configuration for Proof General using PGIP protocol. |
|
21940 | 5 |
See http://proofgeneral.inf.ed.ac.uk/kit |
21637 | 6 |
*) |
7 |
||
8 |
signature PROOF_GENERAL_PGIP = |
|
9 |
sig |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
10 |
val proof_general_emacsN: string |
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
11 |
|
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
12 |
val new_thms_deps: theory -> theory -> string list * string list |
22042
64f8f5433f30
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
aspinall
parents:
22028
diff
changeset
|
13 |
|
28588 | 14 |
val add_preference: string -> Preferences.preference -> unit |
21637 | 15 |
end |
16 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
17 |
structure ProofGeneralPgip : PROOF_GENERAL_PGIP = |
21637 | 18 |
struct |
19 |
||
23641
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
20 |
(** print mode **) |
21637 | 21 |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
22 |
val proof_general_emacsN = "ProofGeneralEmacs"; |
21637 | 23 |
|
23641
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
24 |
|
d6f9d3acffaa
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23621
diff
changeset
|
25 |
(* assembling and issuing PGIP packets *) |
21637 | 26 |
|
32738 | 27 |
val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref; |
28 |
val pgip_refseq = Unsynchronized.ref NONE: int option Unsynchronized.ref; |
|
21637 | 29 |
|
30 |
local |
|
31 |
val pgip_class = "pg" |
|
32 |
val pgip_tag = "Isabelle/Isar" |
|
51963
7e014c16da7d
dummy PGIP id, which appears to be sufficient for PG/Emacs;
wenzelm
parents:
51935
diff
changeset
|
33 |
val pgip_id = "dummy" |
32738 | 34 |
val pgip_seq = Unsynchronized.ref 0 |
35 |
fun pgip_serial () = Unsynchronized.inc pgip_seq |
|
21637 | 36 |
|
37 |
fun assemble_pgips pgips = |
|
51967 | 38 |
PgipOutput.Pgip { tag = SOME pgip_tag, |
21940 | 39 |
class = pgip_class, |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
40 |
seq = pgip_serial (), |
51963
7e014c16da7d
dummy PGIP id, which appears to be sufficient for PG/Emacs;
wenzelm
parents:
51935
diff
changeset
|
41 |
id = pgip_id, |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
42 |
destid = ! pgip_refid, |
21940 | 43 |
(* destid=refid since Isabelle only communicates back to sender *) |
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
44 |
refid = ! pgip_refid, |
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
45 |
refseq = ! pgip_refseq, |
21940 | 46 |
content = pgips } |
21637 | 47 |
in |
48 |
||
51963
7e014c16da7d
dummy PGIP id, which appears to be sufficient for PG/Emacs;
wenzelm
parents:
51935
diff
changeset
|
49 |
fun matching_pgip_id id = (id = pgip_id) |
21637 | 50 |
|
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
51 |
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; |
23759
90bccef65004
Fix nested PGIP messages. Update for schema simplifications.
aspinall
parents:
23723
diff
changeset
|
52 |
|
21637 | 53 |
end; |
54 |
||
28037
915b9a777441
changed Markup print mode to YXML -- explicitly decode messages before being issued;
wenzelm
parents:
28020
diff
changeset
|
55 |
|
21637 | 56 |
|
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
57 |
(* theorem dependencies *) |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
58 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
59 |
local |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
60 |
|
28809 | 61 |
fun add_proof_body (PBody {thms, ...}) = |
28817 | 62 |
thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ())); |
28809 | 63 |
|
64 |
fun add_thm th = |
|
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
65 |
(case Thm.proof_body_of th of |
28809 | 66 |
PBody {proof = PThm (_, ((name, _, _), body)), ...} => |
67 |
if Thm.has_name_hint th andalso Thm.get_name_hint th = name |
|
29635
31d14e9fa0da
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29606
diff
changeset
|
68 |
then add_proof_body (Future.join body) |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
69 |
else I |
28809 | 70 |
| body => add_proof_body body); |
71 |
||
72 |
in |
|
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
73 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
74 |
fun thms_deps ths = |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
75 |
let |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
76 |
(* FIXME proper derivation names!? *) |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
77 |
val names = map Thm.get_name_hint (filter Thm.has_name_hint ths); |
28809 | 78 |
val deps = Symtab.keys (fold add_thm ths Symtab.empty); |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
79 |
in (names, deps) end; |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
80 |
|
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
81 |
fun new_thms_deps thy thy' = |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
82 |
let |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39555
diff
changeset
|
83 |
val prev_facts = Global_Theory.facts_of thy; |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39555
diff
changeset
|
84 |
val facts = Global_Theory.facts_of thy'; |
28100
7650d5e0f8fb
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
wenzelm
parents:
28097
diff
changeset
|
85 |
in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end; |
28097
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
86 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
87 |
end; |
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
88 |
|
003dff7410c1
added new_thms_deps (operates on global facts, some name_hint approximation);
wenzelm
parents:
28066
diff
changeset
|
89 |
|
22216
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
90 |
(* Preferences: tweak for PGIP interfaces *) |
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
91 |
|
32738 | 92 |
val preferences = Unsynchronized.ref Preferences.pure_preferences; |
22216
c3f5aa951a68
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
aspinall
parents:
22171
diff
changeset
|
93 |
|
28066
611e504c1191
extended interface to preferences to allow adding new ones
nipkow
parents:
28037
diff
changeset
|
94 |
fun add_preference cat pref = |
32738 | 95 |
CRITICAL (fn () => Unsynchronized.change preferences (Preferences.add cat pref)); |
28066
611e504c1191
extended interface to preferences to allow adding new ones
nipkow
parents:
28037
diff
changeset
|
96 |
|
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
97 |
fun set_preference pref value = |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
98 |
(case AList.lookup (op =) (map (fn p => (#name p, p)) (maps snd (! preferences))) pref of |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
99 |
SOME {set, ...} => set value |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
100 |
| NONE => error ("Unknown prover preference: " ^ quote pref)); |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
101 |
|
22228
7c27195a4afc
proper use of PureThy.has_name_hint instead of hard-wired string'';
wenzelm
parents:
22225
diff
changeset
|
102 |
|
51965 | 103 |
(** PGIP/Emacs rudiments **) |
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
104 |
|
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
105 |
local |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
106 |
|
51967 | 107 |
fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received"; |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
108 |
|
51935 | 109 |
fun output_emacs pgips = Output.urgent_message (output_pgips pgips); |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
110 |
|
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
111 |
fun process_element_emacs (XML.Elem (("askprefs", _), _)) = |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
112 |
let |
51965 | 113 |
fun preference_of {name, descr, default, pgiptype, get = _, set = _} = |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
114 |
{name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype}; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
115 |
in |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
116 |
! preferences |> List.app (fn (prefcat, prefs) => |
51967 | 117 |
output_emacs |
118 |
[PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}]) |
|
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
119 |
end |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
120 |
| process_element_emacs (XML.Elem (("setpref", attrs), data)) = |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
121 |
let |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
122 |
val name = |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
123 |
(case Properties.get attrs "name" of |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
124 |
SOME name => name |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
125 |
| NONE => invalid_pgip ()); |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
126 |
val value = XML.content_of data; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
127 |
in set_preference name value end |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
128 |
| process_element_emacs _ = invalid_pgip (); |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
129 |
|
21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
130 |
in |
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21646
diff
changeset
|
131 |
|
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
132 |
fun process_pgip_emacs str = |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
133 |
let |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
134 |
val _ = pgip_refid := NONE; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
135 |
val _ = pgip_refseq := NONE; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
136 |
in |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
137 |
(case XML.parse str of |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
138 |
XML.Elem (("pgip", attrs), pgips) => |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
139 |
let |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
140 |
val class = PgipTypes.get_attr "class" attrs; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
141 |
val dest = PgipTypes.get_attr_opt "destid" attrs; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
142 |
val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs); |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
143 |
val processit = |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
144 |
(case dest of |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
145 |
NONE => class = "pa" |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
146 |
| SOME id => matching_pgip_id id); |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
147 |
in |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
148 |
if processit then |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
149 |
(pgip_refid := PgipTypes.get_attr_opt "id" attrs; |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
150 |
pgip_refseq := SOME seq; |
51935 | 151 |
List.app process_element_emacs pgips) |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
152 |
else () |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
153 |
end |
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
154 |
| _ => invalid_pgip ()) |
51967 | 155 |
end handle PgipTypes.PGIP msg => error (msg ^ "\n" ^ str); |
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
156 |
|
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
157 |
val _ = |
48646
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
46961
diff
changeset
|
158 |
Outer_Syntax.improper_command |
91281e9472d8
more official command specifications, including source position;
wenzelm
parents:
46961
diff
changeset
|
159 |
(("ProofGeneral.process_pgip", Keyword.control), Position.none) "(internal)" |
51965 | 160 |
(Parse.text >> (fn str => Toplevel.imperative (fn () => process_pgip_emacs str))); |
38837
b47ee8df7ab4
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
wenzelm
parents:
38833
diff
changeset
|
161 |
|
21637 | 162 |
end; |
51934
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
163 |
|
203a9528bf7a
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
wenzelm
parents:
51933
diff
changeset
|
164 |
end; |