src/Pure/PIDE/isar_document.ML
changeset 44476 e8a87398f35d
parent 44436 546adfa8a6fc
child 44479 9a04e7502e22
--- a/src/Pure/PIDE/isar_document.ML	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 25 16:44:06 2011 +0200
@@ -48,12 +48,15 @@
             end;
 
         val running = Document.cancel_execution state;
-        val (updates, state') = Document.edit old_id new_id edits state;
+        val (assignment, state') = Document.edit old_id new_id edits state;
         val _ = Future.join_tasks running;
         val _ = Document.join_commands state';
         val _ =
           Output.status (Markup.markup (Markup.assign new_id)
-            (implode (map (Markup.markup_only o Markup.edit) updates)));
+            (assignment |>
+              let open XML.Encode
+              in pair (list (pair int int)) (list (pair string (option int))) end
+              |> YXML.string_of_body));
         val state'' = Document.execute new_id state';
       in state'' end));