51 Isabelle_Process.protocol_command "Document.cancel_exec" |
51 Isabelle_Process.protocol_command "Document.cancel_exec" |
52 (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); |
52 (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); |
53 |
53 |
54 val _ = |
54 val _ = |
55 Isabelle_Process.protocol_command "Document.update" |
55 Isabelle_Process.protocol_command "Document.update" |
56 (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
56 (Future.task_context "Document.update" (Future.new_group NONE) |
57 let |
57 (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => |
58 val _ = Execution.discontinue (); |
58 let |
|
59 val _ = Execution.discontinue (); |
59 |
60 |
60 val old_id = Document_ID.parse old_id_string; |
61 val old_id = Document_ID.parse old_id_string; |
61 val new_id = Document_ID.parse new_id_string; |
62 val new_id = Document_ID.parse new_id_string; |
62 val edits = |
63 val edits = |
63 YXML.parse_body edits_yxml |> |
64 YXML.parse_body edits_yxml |> |
64 let open XML.Decode in |
65 let open XML.Decode in |
65 list (pair string |
66 list (pair string |
66 (variant |
67 (variant |
67 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
68 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
68 fn ([], a) => |
69 fn ([], a) => |
69 let |
70 let |
70 val (master, (name, (imports, (keywords, errors)))) = |
71 val (master, (name, (imports, (keywords, errors)))) = |
71 pair string (pair string (pair (list string) |
72 pair string (pair string (pair (list string) |
72 (pair (list (pair string |
73 (pair (list (pair string |
73 (option (pair (pair string (list string)) (list string))))) |
74 (option (pair (pair string (list string)) (list string))))) |
74 (list string)))) a; |
75 (list string)))) a; |
75 val imports' = map (rpair Position.none) imports; |
76 val imports' = map (rpair Position.none) imports; |
76 val header = Thy_Header.make (name, Position.none) imports' keywords; |
77 val header = Thy_Header.make (name, Position.none) imports' keywords; |
77 in Document.Deps (master, header, errors) end, |
78 in Document.Deps (master, header, errors) end, |
78 fn (a :: b, c) => |
79 fn (a :: b, c) => |
79 Document.Perspective (bool_atom a, map int_atom b, |
80 Document.Perspective (bool_atom a, map int_atom b, |
80 list (pair int (pair string (list string))) c)])) |
81 list (pair int (pair string (list string))) c)])) |
81 end; |
82 end; |
82 |
83 |
83 val (removed, assign_update, state') = Document.update old_id new_id edits state; |
84 val (removed, assign_update, state') = Document.update old_id new_id edits state; |
84 val _ = List.app Execution.terminate removed; |
85 val _ = List.app Execution.terminate removed; |
85 val _ = Execution.purge removed; |
86 val _ = Execution.purge removed; |
86 val _ = List.app Isabelle_Process.reset_tracing removed; |
87 val _ = List.app Isabelle_Process.reset_tracing removed; |
87 |
88 |
88 val _ = |
89 val _ = |
89 Output.protocol_message Markup.assign_update |
90 Output.protocol_message Markup.assign_update |
90 [(new_id, assign_update) |> |
91 [(new_id, assign_update) |> |
91 let open XML.Encode |
92 let open XML.Encode |
92 in pair int (list (pair int (list int))) end |
93 in pair int (list (pair int (list int))) end |
93 |> YXML.string_of_body]; |
94 |> YXML.string_of_body]; |
94 in Document.start_execution state' end)); |
95 in Document.start_execution state' end))); |
95 |
96 |
96 val _ = |
97 val _ = |
97 Isabelle_Process.protocol_command "Document.remove_versions" |
98 Isabelle_Process.protocol_command "Document.remove_versions" |
98 (fn [versions_yxml] => Document.change_state (fn state => |
99 (fn [versions_yxml] => Document.change_state (fn state => |
99 let |
100 let |