author | wenzelm |
Thu, 01 Dec 2011 14:29:14 +0100 | |
changeset 45709 | 87017fcbad83 |
parent 45672 | src/Pure/PIDE/isabelle_document.ML@a497c5d4a523 |
child 46119 | 0d7172a7672c |
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 _ = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
11 |
Isabelle_Process.add_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 _ = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
16 |
Isabelle_Process.add_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
|
17 |
(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
|
18 |
|
990ac978854c
explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents:
44610
diff
changeset
|
19 |
val _ = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
20 |
Isabelle_Process.add_command "Document.update_perspective" |
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
21 |
(fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
22 |
let |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
23 |
val old_id = Document.parse_id old_id_string; |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
24 |
val new_id = Document.parse_id new_id_string; |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
25 |
val ids = YXML.parse_body ids_yxml |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
26 |
|> let open XML.Decode in list int end; |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
27 |
|
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
28 |
val _ = Future.join_tasks (Document.cancel_execution state); |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
29 |
in |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
30 |
state |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
31 |
|> Document.update_perspective old_id new_id name ids |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
32 |
|> Document.execute new_id |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
33 |
end)); |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
34 |
|
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
35 |
val _ = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
36 |
Isabelle_Process.add_command "Document.update" |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
37 |
(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
|
38 |
let |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
39 |
val old_id = Document.parse_id old_id_string; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
40 |
val new_id = Document.parse_id new_id_string; |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
41 |
val edits = |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
42 |
YXML.parse_body edits_yxml |> |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
43 |
let open XML.Decode in |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
44 |
list (pair string |
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
45 |
(variant |
44185 | 46 |
[fn ([], []) => Document.Clear, |
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
47 |
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
|
48 |
fn ([], a) => |
44185 | 49 |
Document.Header |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44676
diff
changeset
|
50 |
(Exn.Res |
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44676
diff
changeset
|
51 |
(triple (pair string string) (list string) (list (pair string bool)) a)), |
44384 | 52 |
fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), |
53 |
fn (a, []) => Document.Perspective (map int_atom a)])) |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
54 |
end; |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
55 |
|
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
56 |
val running = Document.cancel_execution state; |
44610
49657380fba6
tuned join_commands: avoid traversing cumulative table;
wenzelm
parents:
44481
diff
changeset
|
57 |
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
|
58 |
val _ = Future.join_tasks running; |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44384
diff
changeset
|
59 |
val _ = |
45666 | 60 |
Output.raw_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
|
61 |
((new_id, assignment) |> |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44436
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
|> YXML.string_of_body); |
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44644
diff
changeset
|
65 |
val state2 = Document.execute new_id state1; |
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44644
diff
changeset
|
66 |
in state2 end)); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
67 |
|
43748 | 68 |
val _ = |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
69 |
Isabelle_Process.add_command "Document.remove_versions" |
44673 | 70 |
(fn [versions_yxml] => Document.change_state (fn state => |
71 |
let |
|
72 |
val versions = |
|
73 |
YXML.parse_body versions_yxml |> |
|
74 |
let open XML.Decode in list int end; |
|
44676 | 75 |
val state1 = Document.remove_versions versions state; |
45666 | 76 |
val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; |
44676 | 77 |
in state1 end)); |
44673 | 78 |
|
79 |
val _ = |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
80 |
Isabelle_Process.add_command "Document.invoke_scala" |
43748 | 81 |
(fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); |
82 |
||
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
83 |
end; |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
84 |