# HG changeset patch
# User wenzelm
# Date 1309859148 -7200
# Node ID 7be2e51928cb6d392b56b07b63e436301ddfb28d
# Parent  573d1272f36d900351ae042bc021053995670132
clarified cancel_execution/await_cancellation;

diff -r 573d1272f36d -r 7be2e51928cb src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Jul 05 11:16:37 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Jul 05 11:45:48 2011 +0200
@@ -18,7 +18,7 @@
   type edit = string * ((command_id option * command_id option) list) option
   type state
   val init_state: state
-  val cancel: state -> unit
+  val cancel_execution: state -> unit -> unit
   val define_command: command_id -> string -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
@@ -185,11 +185,9 @@
 
 (* document execution *)
 
-fun cancel (State {execution, ...}) =
-  List.app Future.cancel execution;
-
-fun await_cancellation (State {execution, ...}) =
-  ignore (Future.join_results execution);
+fun cancel_execution (State {execution, ...}) =
+  (List.app Future.cancel execution;
+    fn () => ignore (Future.join_results execution));
 
 end;
 
@@ -338,20 +336,12 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val _ = cancel state;
-
       val execution' = (* FIXME proper node deps *)
         Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
           [fn () =>
-            let
-              val _ = await_cancellation state;
-              val _ =
-                node_names_of version |> List.app (fn name =>
-                  fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
-                      (get_node version name) ());
-            in () end];
-
-      val _ = await_cancellation state;  (* FIXME async!? *)
+            node_names_of version |> List.app (fn name =>
+              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+                  (get_node version name) ())];
 
     in (versions, commands, execs, execution') end);
 
diff -r 573d1272f36d -r 7be2e51928cb src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Tue Jul 05 11:16:37 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 05 11:45:48 2011 +0200
@@ -30,8 +30,9 @@
                     (XML_Data.dest_option XML_Data.dest_int)
                     (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
 
-      val _ = Document.cancel state;
+      val await_cancellation = Document.cancel_execution state;
       val (updates, state') = Document.edit old_id new_id edits state;
+      val _ = await_cancellation ();
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)
           (implode (map (Markup.markup_only o Markup.edit) updates)));