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