src/Pure/PIDE/protocol.ML
changeset 69845 d28e8199dcb9
parent 68381 2fd3a6d6ba2e
child 69846 e02e3763e7a4
equal deleted inserted replaced
69844:b21ddfa7042b 69845:d28e8199dcb9
   115                 pri = Task_Queue.urgent_pri + 2, interrupts = false}
   115                 pri = Task_Queue.urgent_pri + 2, interrupts = false}
   116                (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
   116                (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed));
   117 
   117 
   118             val _ =
   118             val _ =
   119               Output.protocol_message Markup.assign_update
   119               Output.protocol_message Markup.assign_update
   120                 [(new_id, assign_update) |>
   120                 ((new_id, assign_update) |>
   121                   let open XML.Encode
   121                   let open XML.Encode
   122                   in pair int (list (pair int (list int))) end
   122                   in pair int (list (pair int (list int))) end
   123                   |> YXML.string_of_body];
   123                   |> YXML.chunks_of_body);
   124           in Document.start_execution state' end)));
   124           in Document.start_execution state' end)));
   125 
   125 
   126 val _ =
   126 val _ =
   127   Isabelle_Process.protocol_command "Document.remove_versions"
   127   Isabelle_Process.protocol_command "Document.remove_versions"
   128     (fn [versions_yxml] => Document.change_state (fn state =>
   128     (fn [versions_yxml] => Document.change_state (fn state =>