49 val header = Thy_Header.make (name, Position.none) imports' keywords; |
49 val header = Thy_Header.make (name, Position.none) imports' keywords; |
50 in Document.Deps (master, header, errors) end, |
50 in Document.Deps (master, header, errors) end, |
51 fn (a, []) => Document.Perspective (map int_atom a)])) |
51 fn (a, []) => Document.Perspective (map int_atom a)])) |
52 end; |
52 end; |
53 |
53 |
54 val (assignment, state') = Document.update old_id new_id edits state; |
54 val (assign_update, state') = Document.update old_id new_id edits state; |
55 val _ = |
|
56 Output.protocol_message Markup.assign_update |
|
57 ((new_id, assignment) |> |
|
58 let open XML.Encode |
|
59 in pair int (list (pair int (list int))) end |
|
60 |> YXML.string_of_body); |
|
61 |
55 |
62 val _ = List.app Future.cancel_group (Goal.reset_futures ()); |
56 val _ = List.app Future.cancel_group (Goal.reset_futures ()); |
63 val _ = Exec.purge_unstable (); |
57 val _ = Exec.purge_unstable (); |
64 val _ = Isabelle_Process.reset_tracing (); |
58 val _ = Isabelle_Process.reset_tracing (); |
|
59 |
|
60 val _ = |
|
61 Output.protocol_message Markup.assign_update |
|
62 ((new_id, assign_update) |> |
|
63 let open XML.Encode |
|
64 in pair int (list (pair int (list int))) end |
|
65 |> YXML.string_of_body); |
65 val _ = |
66 val _ = |
66 Event_Timer.request (Time.+ (Time.now (), seconds 0.02)) |
67 Event_Timer.request (Time.+ (Time.now (), seconds 0.02)) |
67 (fn () => Document.start_execution state'); |
68 (fn () => Document.start_execution state'); |
68 in state' end)); |
69 in state' end)); |
69 |
70 |