author | wenzelm |
Mon, 29 Apr 2013 15:47:42 +0200 | |
changeset 51818 | 517f232e867d |
parent 51294 | 0850d43cb355 |
child 52111 | 1fd184eaa310 |
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 _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
11 |
Isabelle_Process.protocol_command "Document.define_command" |
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44612
diff
changeset
|
12 |
(fn [id, name, text] => |
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44612
diff
changeset
|
13 |
Document.change_state (Document.define_command (Document.parse_id id) name text)); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
14 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
15 |
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
|
16 |
Isabelle_Process.protocol_command "Document.discontinue_execution" |
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
17 |
(fn [] => Document.discontinue_execution (Document.state ())); |
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
18 |
|
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
19 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
20 |
Isabelle_Process.protocol_command "Document.cancel_execution" |
47404
e6e5750f1311
simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents:
47388
diff
changeset
|
21 |
(fn [] => Document.cancel_execution (Document.state ())); |
44612
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44610
diff
changeset
|
22 |
|
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44610
diff
changeset
|
23 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
24 |
Isabelle_Process.protocol_command "Document.update" |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
25 |
(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
|
26 |
let |
47404
e6e5750f1311
simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents:
47388
diff
changeset
|
27 |
val _ = Document.cancel_execution state; |
e6e5750f1311
simplified Future.cancel/cancel_group (again) -- running threads only;
wenzelm
parents:
47388
diff
changeset
|
28 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
29 |
val old_id = Document.parse_id old_id_string; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
30 |
val new_id = Document.parse_id new_id_string; |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
31 |
val edits = |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
32 |
YXML.parse_body edits_yxml |> |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
33 |
let open XML.Decode in |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
34 |
list (pair string |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
35 |
(variant |
48755
393a37003851
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
wenzelm
parents:
48707
diff
changeset
|
36 |
[fn ([], []) => Document.Clear, (* FIXME unused !? *) |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
37 |
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
38 |
fn ([], a) => |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
39 |
let |
51294
0850d43cb355
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset
|
40 |
val (master, (name, (imports, (keywords, errors)))) = |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47420
diff
changeset
|
41 |
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
|
42 |
(pair (list (pair string |
3ee314ae1e0a
added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents:
48755
diff
changeset
|
43 |
(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
|
44 |
(list string)))) a; |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48864
diff
changeset
|
45 |
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
|
46 |
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
|
47 |
in Document.Deps (master, header, errors) end, |
44384 | 48 |
fn (a, []) => Document.Perspective (map int_atom a)])) |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
49 |
end; |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
50 |
|
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47404
diff
changeset
|
51 |
val (assignment, state') = Document.update old_id new_id edits state; |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
52 |
val _ = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset
|
53 |
Output.protocol_message Markup.assign_execs |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44660
diff
changeset
|
54 |
((new_id, assignment) |> |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44436
diff
changeset
|
55 |
let open XML.Encode |
47388
fe4b245af74c
discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents:
47346
diff
changeset
|
56 |
in pair int (list (pair int (option int))) end |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44660
diff
changeset
|
57 |
|> YXML.string_of_body); |
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47404
diff
changeset
|
58 |
|
49931
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49647
diff
changeset
|
59 |
val _ = List.app Future.cancel_group (Goal.reset_futures ()); |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50500
diff
changeset
|
60 |
val _ = Isabelle_Process.reset_tracing (); |
47420
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47404
diff
changeset
|
61 |
val _ = Document.start_execution state'; |
0dbe6c69eda2
just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
wenzelm
parents:
47404
diff
changeset
|
62 |
in state' end)); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
63 |
|
43748 | 64 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
65 |
Isabelle_Process.protocol_command "Document.remove_versions" |
44673 | 66 |
(fn [versions_yxml] => Document.change_state (fn state => |
67 |
let |
|
68 |
val versions = |
|
69 |
YXML.parse_body versions_yxml |> |
|
70 |
let open XML.Decode in list int end; |
|
44676 | 71 |
val state1 = Document.remove_versions versions state; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49931
diff
changeset
|
72 |
val _ = Output.protocol_message Markup.removed_versions versions_yxml; |
44676 | 73 |
in state1 end)); |
44673 | 74 |
|
75 |
val _ = |
|
50498 | 76 |
Isabelle_Process.protocol_command "Document.dialog_result" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
77 |
(fn [serial, result] => |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
78 |
Active.dialog_result (Markup.parse_int serial) result |
50498 | 79 |
handle exn => if Exn.is_interrupt exn then () else reraise exn); |
80 |
||
81 |
val _ = |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
82 |
Isabelle_Process.protocol_command "Document.invoke_scala" |
49470 | 83 |
(fn [id, tag, res] => |
84 |
Invoke_Scala.fulfill_method id tag res |
|
85 |
handle exn => if Exn.is_interrupt exn then () else reraise exn); |
|
43748 | 86 |
|
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
87 |
end; |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
88 |