src/Pure/PIDE/isar_document.ML
changeset 45174 061599cb6eb0
parent 45068 458573968568
child 45176 65f60d9ac4bf
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Aug 19 14:01:20 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 19 15:56:26 2011 +0200
     1.3 @@ -30,9 +30,9 @@
     1.4                    fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
     1.5              end;
     1.6  
     1.7 -      val await_cancellation = Document.cancel_execution state;
     1.8 +      val cancellation = Document.cancel_execution state;
     1.9        val (updates, state') = Document.edit old_id new_id edits state;
    1.10 -      val _ = await_cancellation ();
    1.11 +      val _ = Future.join cancellation;
    1.12        val _ = Document.join_commands state';
    1.13        val _ =
    1.14          Output.status (Markup.markup (Markup.assign new_id)