# HG changeset patch
# User wenzelm
# Date 1295987185 -3600
# Node ID a7a93df2366426b52d28d2b5ae0b0a3ab33a1a87
# Parent  5490dc4d999dcb0c9f9eccbcf278ac2fb5b58d2c
singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);

diff -r 5490dc4d999d -r a7a93df23664 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Jan 25 20:06:32 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Jan 25 21:26:25 2011 +0100
@@ -328,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 ();