clarified conditions for node traversal;

--- a/src/Pure/PIDE/command.ML	Mon Jul 29 15:20:02 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 29 15:59:47 2013 +0200
@@ -9,6 +9,7 @@
   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
+  val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   type print
@@ -116,6 +117,8 @@
 
 fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
 
+fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
+
 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
 val eval_result_state = #state o eval_result;
 

--- a/src/Pure/PIDE/document.ML	Mon Jul 29 15:20:02 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 29 15:59:47 2013 +0200
@@ -105,10 +105,10 @@
   | (NONE, NONE) => false
   | _ => true);
 
-fun finished_theory node =
-  (case Exn.capture (Command.eval_result_state o the) (get_result node) of
-    Exn.Res st => can (Toplevel.end_theory Position.none) st
-  | _ => false);
+fun pending_result node =
+  (case get_result node of
+    SOME eval => not (Command.eval_finished eval)
+  | NONE => false);
 
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
@@ -295,9 +295,7 @@
       if Execution.is_running execution_id then
         nodes_of (the_version state version_id) |> String_Graph.schedule
           (fn deps => fn (name, node) =>
-            if not (visible_node node) andalso finished_theory node then
-              Future.value ()
-            else
+            if visible_node node orelse pending_result node then
               (singleton o Future.forks)
                 {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
                   deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
@@ -308,7 +306,8 @@
                         if Execution.is_running execution_id
                         then SOME (Command.exec execution_id exec)
                         else NONE
-                    | NONE => NONE)) node ()))
+                    | NONE => NONE)) node ())
+            else Future.value ())
       else [];
   in () end;
 
@@ -448,6 +447,7 @@
 
     val nodes = nodes_of new_version;
     val is_required = make_required nodes;
+    val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
 
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule
@@ -458,11 +458,10 @@
             (fn () =>
               let
                 val imports = map (apsnd Future.join) deps;
-                val imports_changed = exists (#4 o #1 o #2) imports;
+                val imports_result_changed = exists (#4 o #1 o #2) imports;
                 val node_required = is_required name;
               in
-                if imports_changed orelse AList.defined (op =) edits name orelse
-                  not (finished_theory node)
+                if Symtab.defined edited name orelse visible_node node orelse imports_result_changed
                 then
                   let
                     val node0 = node_of old_version name;
@@ -472,7 +471,7 @@
                       forall (fn (name, (_, node)) => check_theory true name node) imports;
 
                     val (print_execs, common, (still_visible, initial)) =
-                      if imports_changed then (assign_update_empty, NONE, (true, true))
+                      if imports_result_changed then (assign_update_empty, NONE, (true, true))
                       else last_common state node0 node;
                     val common_command_exec = the_default_entry node common;