singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);

--- 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 ();