# HG changeset patch
# User wenzelm
# Date 1375177123 -7200
# Node ID 4ba2e8b9972feb321efd3ac1f12138884dfc8c6a
# Parent  084ac81e987162023b10f07121eff5d8ce020496
de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;

diff -r 084ac81e9871 -r 4ba2e8b9972f src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Jul 29 22:17:32 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Jul 30 11:38:43 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_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
@@ -120,6 +121,7 @@
 
 fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
 
+fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id;
 fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
 
 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
diff -r 084ac81e9871 -r 4ba2e8b9972f src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Jul 29 22:17:32 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Jul 30 11:38:43 2013 +0200
@@ -389,7 +389,7 @@
   is_some (Thy_Info.lookup_theory name) orelse
   can get_header node andalso (not full orelse is_some (get_result node));
 
-fun last_common state node0 node =
+fun last_common state node_required node0 node =
   let
     fun update_flags prev (visible, initial) =
       let
@@ -400,15 +400,17 @@
           | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
       in (visible', initial') end;
 
-    fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) =
-      if same then
+    fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
+      if ok then
         let
-          val flags' = update_flags prev flags;
-          val same' =
+          val flags' as (visible', _) = update_flags prev flags;
+          val ok' =
             (case (lookup_entry node0 command_id, opt_exec) of
-              (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
+              (SOME (eval0, _), SOME (eval, _)) =>
+                Command.eval_eq (eval0, eval) andalso
+                  (visible' orelse node_required orelse Command.eval_running eval)
             | _ => false);
-          val assign_update' = assign_update |> same' ?
+          val assign_update' = assign_update |> ok' ?
             (case opt_exec of
               SOME (eval, prints) =>
                 let
@@ -420,12 +422,12 @@
                   | NONE => I)
                 end
             | NONE => I);
-        in SOME (prev, same', flags', assign_update') end
+        in SOME (prev, ok', flags', assign_update') end
       else NONE;
-    val (common, same, flags, assign_update') =
+    val (common, ok, flags, assign_update') =
       iterate_entries get_common node (NONE, true, (true, true), assign_update_empty);
     val (common', flags') =
-      if same then
+      if ok then
         let val last = Entries.get_after (get_entries node) common
         in (last, update_flags last flags) end
       else (common, flags);
@@ -487,7 +489,7 @@
 
                     val (print_execs, common, (still_visible, initial)) =
                       if imports_result_changed then (assign_update_empty, NONE, (true, true))
-                      else last_common state node0 node;
+                      else last_common state node_required node0 node;
                     val common_command_exec = the_default_entry node common;
 
                     val (updated_execs, (command_id', (eval', _)), _) =
diff -r 084ac81e9871 -r 4ba2e8b9972f src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Jul 29 22:17:32 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Tue Jul 30 11:38:43 2013 +0200
@@ -10,6 +10,7 @@
   val start: unit -> Document_ID.execution
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
+  val is_running_exec: Document_ID.exec -> bool
   val running: Document_ID.execution -> Document_ID.exec -> bool
   val cancel: Document_ID.exec -> unit
   val terminate: Document_ID.exec -> unit
@@ -39,6 +40,9 @@
 
 (* registered execs *)
 
+fun is_running_exec exec_id =
+  Inttab.defined (snd (Synchronized.value state)) exec_id;
+
 fun running execution_id exec_id =
   Synchronized.guarded_access state
     (fn (execution_id', execs) =>