# HG changeset patch
# User wenzelm
# Date 1295990103 -3600
# Node ID eb512b67a836d1f06b56e9744c5b329f03e78f6d
# Parent  a7a93df2366426b52d28d2b5ae0b0a3ab33a1a87# Parent  8ff597b3dd80e86e5aa16c18687aadf17141293c
merged

diff -r 8ff597b3dd80 -r eb512b67a836 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Jan 25 14:06:43 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Jan 25 22:15:03 2011 +0100
@@ -284,6 +284,7 @@
 fun edit (old_id: version_id) (new_id: version_id) edits state =
   let
     val old_version = the_version state old_id;
+    val _ = Time.now ();  (* FIXME odd workaround *)
     val new_version = fold edit_nodes edits old_version;
 
     fun update_node name (rev_updates, version, st) =
@@ -327,11 +328,14 @@
       fun await_cancellation () = Future.join_results execution;
 
       val execution' = (* FIXME proper node deps *)
-        node_names_of version |> map (fn name =>
-          Future.fork_pri 1 (fn () =>
-            (await_cancellation ();
-              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
-                (get_node version name) ())));
+        [Future.fork_pri 1 (fn () =>
+          let
+            val _ = await_cancellation ();
+            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 ();