equal
deleted
inserted
replaced
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Protocol message formats for interactive Isar documents. |
4 Protocol message formats for interactive Isar documents. |
5 *) |
5 *) |
6 |
6 |
7 signature ISAR_DOCUMENT = |
7 structure Isar_Document: sig end = |
8 sig |
|
9 val state: unit -> Document.state |
|
10 end |
|
11 |
|
12 structure Isar_Document: ISAR_DOCUMENT = |
|
13 struct |
8 struct |
14 |
|
15 val global_state = Synchronized.var "Isar_Document" Document.init_state; |
|
16 val change_state = Synchronized.change global_state; |
|
17 |
|
18 fun state () = Synchronized.value global_state; |
|
19 |
9 |
20 val _ = |
10 val _ = |
21 Isabelle_Process.add_command "Isar_Document.define_command" |
11 Isabelle_Process.add_command "Isar_Document.define_command" |
22 (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text)); |
12 (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text)); |
23 |
13 |
24 val _ = |
14 val _ = |
25 Isabelle_Process.add_command "Isar_Document.edit_version" |
15 Isabelle_Process.add_command "Isar_Document.edit_version" |
26 (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state => |
16 (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
27 let |
17 let |
28 val old_id = Document.parse_id old_id_string; |
18 val old_id = Document.parse_id old_id_string; |
29 val new_id = Document.parse_id new_id_string; |
19 val new_id = Document.parse_id new_id_string; |
30 val edits = |
20 val edits = |
31 XML_Data.dest_list |
21 XML_Data.dest_list |