72 (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); |
72 (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); |
73 |
73 |
74 val _ = |
74 val _ = |
75 Isabelle_Process.protocol_command "Document.update" |
75 Isabelle_Process.protocol_command "Document.update" |
76 (Future.task_context "Document.update" (Future.new_group NONE) |
76 (Future.task_context "Document.update" (Future.new_group NONE) |
77 (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] => |
77 (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => |
78 Document.change_state (fn state => |
78 Document.change_state (fn state => |
79 let |
79 let |
80 val old_id = Document_ID.parse old_id_string; |
80 val old_id = Document_ID.parse old_id_string; |
81 val new_id = Document_ID.parse new_id_string; |
81 val new_id = Document_ID.parse new_id_string; |
|
82 val consolidate = |
|
83 YXML.parse_body consolidate_yxml |> |
|
84 let open XML.Decode in list string end; |
82 val edits = |
85 val edits = |
83 YXML.parse_body edits_yxml |> |
86 edits_yxml |> map (YXML.parse_body #> |
84 let open XML.Decode in |
87 let open XML.Decode in |
85 list (pair string |
88 pair string |
86 (variant |
89 (variant |
87 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
90 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
88 fn ([], a) => |
91 fn ([], a) => |
89 let |
92 let |
90 val (master, (name, (imports, (keywords, errors)))) = |
93 val (master, (name, (imports, (keywords, errors)))) = |
96 val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; |
99 val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; |
97 val header = Thy_Header.make (name, Position.none) imports' keywords'; |
100 val header = Thy_Header.make (name, Position.none) imports' keywords'; |
98 in Document.Deps {master = master, header = header, errors = errors} end, |
101 in Document.Deps {master = master, header = header, errors = errors} end, |
99 fn (a :: b, c) => |
102 fn (a :: b, c) => |
100 Document.Perspective (bool_atom a, map int_atom b, |
103 Document.Perspective (bool_atom a, map int_atom b, |
101 list (pair int (pair string (list string))) c)])) |
104 list (pair int (pair string (list string))) c)]) |
102 end; |
105 end); |
103 val consolidate = |
|
104 YXML.parse_body consolidate_yxml |> |
|
105 let open XML.Decode in list string end; |
|
106 |
106 |
107 val _ = Execution.discontinue (); |
107 val _ = Execution.discontinue (); |
108 |
108 |
109 val (removed, assign_update, state') = |
109 val (removed, assign_update, state') = |
110 Document.update old_id new_id edits consolidate state; |
110 Document.update old_id new_id edits consolidate state; |