author | wenzelm |
Fri, 06 Apr 2012 11:49:08 +0200 | |
changeset 47346 | cd3ab7625519 |
parent 47343 | b8aeab386414 |
child 47388 | fe4b245af74c |
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" |
44612
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44610
diff
changeset
|
21 |
(fn [] => ignore (Document.cancel_execution (Document.state ()))); |
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 |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
27 |
val old_id = Document.parse_id old_id_string; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
28 |
val new_id = Document.parse_id new_id_string; |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
29 |
val edits = |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
30 |
YXML.parse_body edits_yxml |> |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
31 |
let open XML.Decode in |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
32 |
list (pair string |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
33 |
(variant |
44185 | 34 |
[fn ([], []) => Document.Clear, |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
35 |
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
|
36 |
fn ([], a) => |
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
37 |
let |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
38 |
val ((((master, name), imports), keywords), uses) = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
39 |
pair (pair (pair (pair string string) (list string)) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
40 |
(list (pair string (option (pair string (list string)))))) |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
41 |
(list (pair string bool)) a; |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
42 |
val res = |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
43 |
Exn.capture (fn () => |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
44 |
(master, Thy_Header.make name imports keywords |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
45 |
(map (apfst Path.explode) uses))) (); |
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset
|
46 |
in Document.Header res end, |
44384 | 47 |
fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), |
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 |
|
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
51 |
val running = Document.cancel_execution state; |
44610
49657380fba6
tuned join_commands: avoid traversing cumulative table;
wenzelm
parents:
44481
diff
changeset
|
52 |
val (assignment, state1) = 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
|
53 |
val _ = Future.join_tasks running; |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
54 |
val _ = |
46774 | 55 |
Output.protocol_message Isabelle_Markup.assign_execs |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44660
diff
changeset
|
56 |
((new_id, assignment) |> |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44436
diff
changeset
|
57 |
let open XML.Encode |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44660
diff
changeset
|
58 |
in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44660
diff
changeset
|
59 |
|> YXML.string_of_body); |
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44644
diff
changeset
|
60 |
val state2 = Document.execute new_id state1; |
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44644
diff
changeset
|
61 |
in state2 end)); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
62 |
|
43748 | 63 |
val _ = |
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
64 |
Isabelle_Process.protocol_command "Document.remove_versions" |
44673 | 65 |
(fn [versions_yxml] => Document.change_state (fn state => |
66 |
let |
|
67 |
val versions = |
|
68 |
YXML.parse_body versions_yxml |> |
|
69 |
let open XML.Decode in list int end; |
|
44676 | 70 |
val state1 = Document.remove_versions versions state; |
46774 | 71 |
val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml; |
44676 | 72 |
in state1 end)); |
44673 | 73 |
|
74 |
val _ = |
|
46119
0d7172a7672c
tuned signature -- emphasize special nature of protocol commands;
wenzelm
parents:
45709
diff
changeset
|
75 |
Isabelle_Process.protocol_command "Document.invoke_scala" |
43748 | 76 |
(fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); |
77 |
||
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
78 |
end; |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
79 |