|
1 (* Title: Pure/PIDE/protocol.ML |
|
2 Author: Makarius |
|
3 |
|
4 Protocol message formats for interactive proof documents. |
|
5 *) |
|
6 |
|
7 structure Protocol: sig end = |
|
8 struct |
|
9 |
|
10 val _ = |
|
11 Isabelle_Process.add_command "Document.define_command" |
|
12 (fn [id, name, text] => |
|
13 Document.change_state (Document.define_command (Document.parse_id id) name text)); |
|
14 |
|
15 val _ = |
|
16 Isabelle_Process.add_command "Document.cancel_execution" |
|
17 (fn [] => ignore (Document.cancel_execution (Document.state ()))); |
|
18 |
|
19 val _ = |
|
20 Isabelle_Process.add_command "Document.update_perspective" |
|
21 (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => |
|
22 let |
|
23 val old_id = Document.parse_id old_id_string; |
|
24 val new_id = Document.parse_id new_id_string; |
|
25 val ids = YXML.parse_body ids_yxml |
|
26 |> let open XML.Decode in list int end; |
|
27 |
|
28 val _ = Future.join_tasks (Document.cancel_execution state); |
|
29 in |
|
30 state |
|
31 |> Document.update_perspective old_id new_id name ids |
|
32 |> Document.execute new_id |
|
33 end)); |
|
34 |
|
35 val _ = |
|
36 Isabelle_Process.add_command "Document.update" |
|
37 (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
|
38 let |
|
39 val old_id = Document.parse_id old_id_string; |
|
40 val new_id = Document.parse_id new_id_string; |
|
41 val edits = |
|
42 YXML.parse_body edits_yxml |> |
|
43 let open XML.Decode in |
|
44 list (pair string |
|
45 (variant |
|
46 [fn ([], []) => Document.Clear, |
|
47 fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
|
48 fn ([], a) => |
|
49 Document.Header |
|
50 (Exn.Res |
|
51 (triple (pair string string) (list string) (list (pair string bool)) a)), |
|
52 fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), |
|
53 fn (a, []) => Document.Perspective (map int_atom a)])) |
|
54 end; |
|
55 |
|
56 val running = Document.cancel_execution state; |
|
57 val (assignment, state1) = Document.update old_id new_id edits state; |
|
58 val _ = Future.join_tasks running; |
|
59 val _ = |
|
60 Output.raw_message Isabelle_Markup.assign_execs |
|
61 ((new_id, assignment) |> |
|
62 let open XML.Encode |
|
63 in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end |
|
64 |> YXML.string_of_body); |
|
65 val state2 = Document.execute new_id state1; |
|
66 in state2 end)); |
|
67 |
|
68 val _ = |
|
69 Isabelle_Process.add_command "Document.remove_versions" |
|
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; |
|
75 val state1 = Document.remove_versions versions state; |
|
76 val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; |
|
77 in state1 end)); |
|
78 |
|
79 val _ = |
|
80 Isabelle_Process.add_command "Document.invoke_scala" |
|
81 (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); |
|
82 |
|
83 end; |
|
84 |