# HG changeset patch
# User wenzelm
# Date 1373553337 -7200
# Node ID 55e62a25a7cefe358d0f631d15fb0605bb3313b5
# Parent  75afb82daf5c1ed3b98a79c34188546a05228e22
tuned -- cleanup before publishing assignment;

diff -r 75afb82daf5c -r 55e62a25a7ce src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Jul 11 16:26:14 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Jul 11 16:35:37 2013 +0200
@@ -51,17 +51,18 @@
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
-        val (assignment, state') = Document.update old_id new_id edits state;
-        val _ =
-          Output.protocol_message Markup.assign_update
-            ((new_id, assignment) |>
-              let open XML.Encode
-              in pair int (list (pair int (list int))) end
-              |> YXML.string_of_body);
+        val (assign_update, state') = Document.update old_id new_id edits state;
 
         val _ = List.app Future.cancel_group (Goal.reset_futures ());
         val _ = Exec.purge_unstable ();
         val _ = Isabelle_Process.reset_tracing ();
+
+        val _ =
+          Output.protocol_message Markup.assign_update
+            ((new_id, assign_update) |>
+              let open XML.Encode
+              in pair int (list (pair int (list int))) end
+              |> YXML.string_of_body);
         val _ =
           Event_Timer.request (Time.+ (Time.now (), seconds 0.02))
             (fn () => Document.start_execution state');