author | wenzelm |
Sun, 24 May 2020 10:36:42 +0200 | |
changeset 71875 | aaa984499d36 |
parent 71024 | 38bed2483e6a |
child 71876 | ad063ac1f617 |
permissions | -rw-r--r-- |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
1 |
(* Title: Pure/PIDE/protocol.ML |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
4 |
Protocol message formats for interactive proof documents. |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
5 |
*) |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
7 |
structure Protocol: sig end = |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
8 |
struct |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
9 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
10 |
val _ = |
56387 | 11 |
Isabelle_Process.protocol_command "Prover.echo" |
52786 | 12 |
(fn args => List.app writeln args); |
13 |
||
14 |
val _ = |
|
56387 | 15 |
Isabelle_Process.protocol_command "Prover.options" |
52786 | 16 |
(fn [options_yxml] => |
65300 | 17 |
(Options.set_default (Options.decode (YXML.parse_body options_yxml)); |
18 |
Isabelle_Process.init_options_interactive ())); |
|
52585 | 19 |
|
20 |
val _ = |
|
71875 | 21 |
Isabelle_Process.protocol_command "Prover.init_session" |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70665
diff
changeset
|
22 |
(fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml, |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
23 |
loaded_theories_yxml] => |
65470 | 24 |
let |
25 |
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end; |
|
66712 | 26 |
val decode_list = YXML.parse_body #> let open XML.Decode in list string end; |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
27 |
val decode_sessions = |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
28 |
YXML.parse_body #> let open XML.Decode in list (pair string properties) end; |
65470 | 29 |
in |
71875 | 30 |
Resources.init_session |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70665
diff
changeset
|
31 |
{session_positions = decode_sessions session_positions_yxml, |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70665
diff
changeset
|
32 |
session_directories = decode_table session_directories_yxml, |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
33 |
docs = decode_list doc_names_yxml, |
67219 | 34 |
global_theories = decode_table global_theories_yxml, |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
35 |
loaded_theories = decode_list loaded_theories_yxml} |
65470 | 36 |
end); |
37 |
||
38 |
val _ = |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
39 |
Isabelle_Process.protocol_command "Document.define_blob" |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
40 |
(fn [digest, content] => Document.change_state (Document.define_blob digest content)); |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
41 |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
42 |
fun decode_command id name blobs_xml toks_xml sources : Document.command = |
70663 | 43 |
let |
44 |
open XML.Decode; |
|
45 |
val (blobs_digests, blobs_index) = |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
46 |
blobs_xml |> |
70663 | 47 |
let |
48 |
val message = YXML.string_of_body o Protocol_Message.command_positions id; |
|
49 |
in |
|
50 |
pair |
|
51 |
(list (variant |
|
52 |
[fn ([], a) => Exn.Res (pair string (option string) a), |
|
53 |
fn ([], a) => Exn.Exn (ERROR (message a))])) |
|
54 |
int |
|
55 |
end; |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
56 |
val toks = list (pair int int) toks_xml; |
70663 | 57 |
in |
58 |
{command_id = Document_ID.parse id, |
|
59 |
name = name, |
|
60 |
blobs_digests = blobs_digests, |
|
61 |
blobs_index = blobs_index, |
|
62 |
tokens = toks ~~ sources} |
|
63 |
end; |
|
64 |
||
71024 | 65 |
fun commands_accepted ids = |
66 |
Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; |
|
70665
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
67 |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
68 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
69 |
Isabelle_Process.protocol_command "Document.define_command" |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
70 |
(fn id :: name :: blobs :: toks :: sources => |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
71 |
let |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
72 |
val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; |
70665
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
73 |
val _ = Document.change_state (Document.define_command command); |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
74 |
in commands_accepted [id] end); |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
75 |
|
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
76 |
val _ = |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
77 |
Isabelle_Process.protocol_command "Document.define_commands" |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
78 |
(fn args => |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
79 |
let |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
80 |
fun decode arg = |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
81 |
let |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
82 |
open XML.Decode; |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
83 |
val (id, (name, (blobs_xml, (toks_xml, sources)))) = |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
84 |
pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70663
diff
changeset
|
85 |
in decode_command id name blobs_xml toks_xml sources end; |
70665
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
86 |
|
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
87 |
val commands = map decode args; |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
88 |
val _ = Document.change_state (fold Document.define_command commands); |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
89 |
in commands_accepted (map (Value.print_int o #command_id) commands) end); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
90 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
91 |
val _ = |
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
92 |
Isabelle_Process.protocol_command "Document.discontinue_execution" |
52606 | 93 |
(fn [] => Execution.discontinue ()); |
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
94 |
|
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
95 |
val _ = |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
96 |
Isabelle_Process.protocol_command "Document.cancel_exec" |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
97 |
(fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
98 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
99 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
100 |
Isabelle_Process.protocol_command "Document.update" |
59370
b13ff987c559
refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;
wenzelm
parents:
59366
diff
changeset
|
101 |
(Future.task_context "Document.update" (Future.new_group NONE) |
69849 | 102 |
(fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => |
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
103 |
Document.change_state (fn state => |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
104 |
let |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
105 |
val old_id = Document_ID.parse old_id_string; |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
106 |
val new_id = Document_ID.parse new_id_string; |
69849 | 107 |
val consolidate = |
108 |
YXML.parse_body consolidate_yxml |> |
|
109 |
let open XML.Decode in list string end; |
|
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
110 |
val edits = |
69849 | 111 |
edits_yxml |> map (YXML.parse_body #> |
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
112 |
let open XML.Decode in |
69849 | 113 |
pair string |
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
114 |
(variant |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
115 |
[fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
116 |
fn ([], a) => |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
117 |
let |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
118 |
val (master, (name, (imports, (keywords, errors)))) = |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
119 |
pair string (pair string (pair (list string) |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
120 |
(pair (list (pair string |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
121 |
(pair (pair string (list string)) (list string)))) |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
122 |
(list YXML.string_of_body)))) a; |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
123 |
val imports' = map (rpair Position.none) imports; |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
124 |
val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
125 |
val header = Thy_Header.make (name, Position.none) imports' keywords'; |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
126 |
in Document.Deps {master = master, header = header, errors = errors} end, |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
127 |
fn (a :: b, c) => |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
128 |
Document.Perspective (bool_atom a, map int_atom b, |
69849 | 129 |
list (pair int (pair string (list string))) c)]) |
130 |
end); |
|
47404
e6e5750f1311
simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents:
47388
diff
changeset
|
131 |
|
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
132 |
val _ = Execution.discontinue (); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
133 |
|
70284
3e17c3a5fd39
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents:
69849
diff
changeset
|
134 |
val (edited, removed, assign_update, state') = |
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
135 |
Document.update old_id new_id edits consolidate state; |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
136 |
val _ = |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
137 |
(singleton o Future.forks) |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
138 |
{name = "Document.update/remove", group = NONE, |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
139 |
deps = Execution.snapshot removed, |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
140 |
pri = Task_Queue.urgent_pri + 2, interrupts = false} |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
141 |
(fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); |
52601 | 142 |
|
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
143 |
val _ = |
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
144 |
Output.protocol_message Markup.assign_update |
70284
3e17c3a5fd39
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents:
69849
diff
changeset
|
145 |
((new_id, edited, assign_update) |> |
69846 | 146 |
let |
147 |
open XML.Encode; |
|
148 |
fun encode_upd (a, bs) = |
|
149 |
string (space_implode "," (map Value.print_int (a :: bs))); |
|
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70712
diff
changeset
|
150 |
in triple int (list string) (list encode_upd) end); |
68336
09ac56914b29
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
wenzelm
parents:
67493
diff
changeset
|
151 |
in Document.start_execution state' end))); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
152 |
|
43748 | 153 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
154 |
Isabelle_Process.protocol_command "Document.remove_versions" |
44673 | 155 |
(fn [versions_yxml] => Document.change_state (fn state => |
156 |
let |
|
157 |
val versions = |
|
158 |
YXML.parse_body versions_yxml |> |
|
159 |
let open XML.Decode in list int end; |
|
44676 | 160 |
val state1 = Document.remove_versions versions state; |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70712
diff
changeset
|
161 |
val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)]; |
44676 | 162 |
in state1 end)); |
44673 | 163 |
|
164 |
val _ = |
|
50498 | 165 |
Isabelle_Process.protocol_command "Document.dialog_result" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
166 |
(fn [serial, result] => |
63806 | 167 |
Active.dialog_result (Value.parse_int serial) result |
62505 | 168 |
handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); |
50498 | 169 |
|
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
170 |
val _ = |
62467 | 171 |
Isabelle_Process.protocol_command "ML_Heap.share_common_data" |
172 |
(fn [] => ML_Heap.share_common_data ()); |
|
57868
0b954ac94827
protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
wenzelm
parents:
56616
diff
changeset
|
173 |
|
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
174 |
end; |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
175 |