stop node execution at first unassigned exec;

--- a/src/Pure/PIDE/document.ML	Fri Apr 06 11:49:08 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Apr 06 12:02:24 2012 +0200
@@ -241,7 +241,7 @@
 
 
 
-(** global state -- document structure and execution process **)
+(** document state -- content structure and execution process **)
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
@@ -316,19 +316,18 @@
     let
       val version = the_version state version_id;
 
+      fun run node command_id exec =
+        let
+          val (_, print) = Command.memo_eval exec;
+          val _ =
+            if visible_command node command_id
+            then ignore (Lazy.future Future.default_params print)
+            else ();
+        in () end;
+
       val group = Future.new_group NONE;
       val running = Unsynchronized.ref true;
 
-      fun run _ _ NONE = ()
-        | run node command_id (SOME (_, exec)) =
-            let
-              val (_, print) = Command.memo_eval exec;
-              val _ =
-                if visible_command node command_id
-                then ignore (Lazy.future Future.default_params print)
-                else ();
-            in () end;
-
       val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
@@ -339,8 +338,10 @@
                 {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
                   deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
                 (fn () =>
-                  iterate_entries (fn ((_, id), exec) => fn () =>
-                    if ! running then SOME (run node id exec) else NONE) node ()));
+                  iterate_entries (fn ((_, id), opt_exec) => fn () =>
+                    (case opt_exec of
+                      SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
+                    | NONE => NONE)) node ()));
 
     in (versions, commands, (version_id, group, running)) end);