6 |
6 |
7 structure Protocol: sig end = |
7 structure Protocol: sig end = |
8 struct |
8 struct |
9 |
9 |
10 val _ = |
10 val _ = |
11 Isabelle_Process.add_command "Document.define_command" |
11 Isabelle_Process.protocol_command "Document.define_command" |
12 (fn [id, name, text] => |
12 (fn [id, name, text] => |
13 Document.change_state (Document.define_command (Document.parse_id id) name text)); |
13 Document.change_state (Document.define_command (Document.parse_id id) name text)); |
14 |
14 |
15 val _ = |
15 val _ = |
16 Isabelle_Process.add_command "Document.cancel_execution" |
16 Isabelle_Process.protocol_command "Document.cancel_execution" |
17 (fn [] => ignore (Document.cancel_execution (Document.state ()))); |
17 (fn [] => ignore (Document.cancel_execution (Document.state ()))); |
18 |
18 |
19 val _ = |
19 val _ = |
20 Isabelle_Process.add_command "Document.update_perspective" |
20 Isabelle_Process.protocol_command "Document.update_perspective" |
21 (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => |
21 (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => |
22 let |
22 let |
23 val old_id = Document.parse_id old_id_string; |
23 val old_id = Document.parse_id old_id_string; |
24 val new_id = Document.parse_id new_id_string; |
24 val new_id = Document.parse_id new_id_string; |
25 val ids = YXML.parse_body ids_yxml |
25 val ids = YXML.parse_body ids_yxml |
31 |> Document.update_perspective old_id new_id name ids |
31 |> Document.update_perspective old_id new_id name ids |
32 |> Document.execute new_id |
32 |> Document.execute new_id |
33 end)); |
33 end)); |
34 |
34 |
35 val _ = |
35 val _ = |
36 Isabelle_Process.add_command "Document.update" |
36 Isabelle_Process.protocol_command "Document.update" |
37 (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
37 (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
38 let |
38 let |
39 val old_id = Document.parse_id old_id_string; |
39 val old_id = Document.parse_id old_id_string; |
40 val new_id = Document.parse_id new_id_string; |
40 val new_id = Document.parse_id new_id_string; |
41 val edits = |
41 val edits = |
64 |> YXML.string_of_body); |
64 |> YXML.string_of_body); |
65 val state2 = Document.execute new_id state1; |
65 val state2 = Document.execute new_id state1; |
66 in state2 end)); |
66 in state2 end)); |
67 |
67 |
68 val _ = |
68 val _ = |
69 Isabelle_Process.add_command "Document.remove_versions" |
69 Isabelle_Process.protocol_command "Document.remove_versions" |
70 (fn [versions_yxml] => Document.change_state (fn state => |
70 (fn [versions_yxml] => Document.change_state (fn state => |
71 let |
71 let |
72 val versions = |
72 val versions = |
73 YXML.parse_body versions_yxml |> |
73 YXML.parse_body versions_yxml |> |
74 let open XML.Decode in list int end; |
74 let open XML.Decode in list int end; |
75 val state1 = Document.remove_versions versions state; |
75 val state1 = Document.remove_versions versions state; |
76 val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; |
76 val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; |
77 in state1 end)); |
77 in state1 end)); |
78 |
78 |
79 val _ = |
79 val _ = |
80 Isabelle_Process.add_command "Document.invoke_scala" |
80 Isabelle_Process.protocol_command "Document.invoke_scala" |
81 (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); |
81 (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); |
82 |
82 |
83 end; |
83 end; |
84 |
84 |