author | wenzelm |
Thu, 17 Apr 2014 13:21:36 +0200 | |
changeset 56616 | abc2da18d08d |
parent 56458 | a8d960baa5c2 |
child 57868 | 0b954ac94827 |
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] => |
17 |
let val options = Options.decode (YXML.parse_body options_yxml) in |
|
18 |
Options.set_default options; |
|
19 |
Future.ML_statistics := true; |
|
20 |
Multithreading.trace := Options.int options "threads_trace"; |
|
54717 | 21 |
Multithreading.max_threads_update (Options.int options "threads"); |
52786 | 22 |
Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0) |
23 |
end); |
|
52585 | 24 |
|
25 |
val _ = |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
26 |
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
|
27 |
(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
|
28 |
|
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
29 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
30 |
Isabelle_Process.protocol_command "Document.define_command" |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
31 |
(fn [id, name, blobs_yxml, text] => |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
32 |
let |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
33 |
val blobs = |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
34 |
YXML.parse_body blobs_yxml |> |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
35 |
let open XML.Decode in |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
36 |
list (variant |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56447
diff
changeset
|
37 |
[fn ([], a) => Exn.Res (pair string (option string) a), |
54526 | 38 |
fn ([], a) => Exn.Exn (ERROR (string a))]) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
39 |
end; |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
40 |
in |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
41 |
Document.change_state (Document.define_command (Document_ID.parse id) name blobs text) |
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
53192
diff
changeset
|
42 |
end); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
43 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
44 |
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
|
45 |
Isabelle_Process.protocol_command "Document.discontinue_execution" |
52606 | 46 |
(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
|
47 |
|
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
48 |
val _ = |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
49 |
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
|
50 |
(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
|
51 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
52 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
53 |
Isabelle_Process.protocol_command "Document.update" |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
54 |
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
55 |
let |
52606 | 56 |
val _ = Execution.discontinue (); |
47404
e6e5750f1311
simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents:
47388
diff
changeset
|
57 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
58 |
val old_id = Document_ID.parse old_id_string; |
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
59 |
val new_id = Document_ID.parse new_id_string; |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
60 |
val edits = |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
61 |
YXML.parse_body edits_yxml |> |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
62 |
let open XML.Decode in |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
63 |
list (pair string |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
64 |
(variant |
54562
301a721af68b
clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
wenzelm
parents:
54526
diff
changeset
|
65 |
[fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
66 |
fn ([], a) => |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
67 |
let |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
68 |
val (master, (name, (imports, (keywords, errors)))) = |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47420
diff
changeset
|
69 |
pair string (pair string (pair (list string) |
48864
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48755
diff
changeset
|
70 |
(pair (list (pair string |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48755
diff
changeset
|
71 |
(option (pair (pair string (list string)) (list string))))) |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
72 |
(list string)))) a; |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48864
diff
changeset
|
73 |
val imports' = map (rpair Position.none) imports; |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
74 |
val header = Thy_Header.make (name, Position.none) imports' keywords; |
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
75 |
in Document.Deps (master, header, errors) end, |
52849 | 76 |
fn (a :: b, c) => |
77 |
Document.Perspective (bool_atom a, map int_atom b, |
|
52862
930ce8eacb87
tuned signature -- more uniform treatment of overlays as command mapping;
wenzelm
parents:
52849
diff
changeset
|
78 |
list (pair int (pair string (list string))) c)])) |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
79 |
end; |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
80 |
|
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
81 |
val (removed, assign_update, state') = Document.update old_id new_id edits state; |
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
82 |
val _ = List.app Execution.terminate removed; |
53192 | 83 |
val _ = Execution.purge removed; |
52655
3b2b1ef13979
more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents:
52607
diff
changeset
|
84 |
val _ = List.app Isabelle_Process.reset_tracing removed; |
52601 | 85 |
|
86 |
val _ = |
|
87 |
Output.protocol_message Markup.assign_update |
|
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
54717
diff
changeset
|
88 |
[(new_id, assign_update) |> |
52601 | 89 |
let open XML.Encode |
90 |
in pair int (list (pair int (list int))) end |
|
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
54717
diff
changeset
|
91 |
|> YXML.string_of_body]; |
52774
627fb639a2d9
maintain explicit execution frontier: avoid conflict with former task via static dependency;
wenzelm
parents:
52765
diff
changeset
|
92 |
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
|
93 |
|
43748 | 94 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
95 |
Isabelle_Process.protocol_command "Document.remove_versions" |
44673 | 96 |
(fn [versions_yxml] => Document.change_state (fn state => |
97 |
let |
|
98 |
val versions = |
|
99 |
YXML.parse_body versions_yxml |> |
|
100 |
let open XML.Decode in list int end; |
|
44676 | 101 |
val state1 = Document.remove_versions versions state; |
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
54717
diff
changeset
|
102 |
val _ = Output.protocol_message Markup.removed_versions [versions_yxml]; |
44676 | 103 |
in state1 end)); |
44673 | 104 |
|
105 |
val _ = |
|
50498 | 106 |
Isabelle_Process.protocol_command "Document.dialog_result" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
107 |
(fn [serial, result] => |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
108 |
Active.dialog_result (Markup.parse_int serial) result |
52775
e0169f13bd37
keep memo_exec execution running, which is important to cancel goal forks eventually;
wenzelm
parents:
52774
diff
changeset
|
109 |
handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn); |
50498 | 110 |
|
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
111 |
val _ = |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
112 |
Isabelle_Process.protocol_command "use_theories" |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
113 |
(fn id :: master_dir :: thys => |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
114 |
let |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
115 |
val result = |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
116 |
Exn.capture (fn () => |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
117 |
Thy_Info.use_theories |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
118 |
{document = false, last_timing = K NONE, master_dir = Path.explode master_dir} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
119 |
(map (rpair Position.none) thys)) (); |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
120 |
val ok = |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
121 |
(case result of |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
122 |
Exn.Res _ => true |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
123 |
| Exn.Exn exn => (Runtime.exn_error_message exn; false)); |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
124 |
in Output.protocol_message (Markup.use_theories_result id ok) [] end); |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56458
diff
changeset
|
125 |
|
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
126 |
end; |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
127 |