1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 22:17:32 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 30 11:38:43 2013 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     1.5    type eval
     1.6    val eval_eq: eval * eval -> bool
     1.7 +  val eval_running: eval -> bool
     1.8    val eval_finished: eval -> bool
     1.9    val eval_result_state: eval -> Toplevel.state
    1.10    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.11 @@ -120,6 +121,7 @@
    1.12  
    1.13  fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.14  
    1.15 +fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id;
    1.16  fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
    1.17  
    1.18  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;

     2.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 22:17:32 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 30 11:38:43 2013 +0200
     2.3 @@ -389,7 +389,7 @@
     2.4    is_some (Thy_Info.lookup_theory name) orelse
     2.5    can get_header node andalso (not full orelse is_some (get_result node));
     2.6  
     2.7 -fun last_common state node0 node =
     2.8 +fun last_common state node_required node0 node =
     2.9    let
    2.10      fun update_flags prev (visible, initial) =
    2.11        let
    2.12 @@ -400,15 +400,17 @@
    2.13            | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
    2.14        in (visible', initial') end;
    2.15  
    2.16 -    fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) =
    2.17 -      if same then
    2.18 +    fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
    2.19 +      if ok then
    2.20          let
    2.21 -          val flags' = update_flags prev flags;
    2.22 -          val same' =
    2.23 +          val flags' as (visible', _) = update_flags prev flags;
    2.24 +          val ok' =
    2.25              (case (lookup_entry node0 command_id, opt_exec) of
    2.26 -              (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
    2.27 +              (SOME (eval0, _), SOME (eval, _)) =>
    2.28 +                Command.eval_eq (eval0, eval) andalso
    2.29 +                  (visible' orelse node_required orelse Command.eval_running eval)
    2.30              | _ => false);
    2.31 -          val assign_update' = assign_update |> same' ?
    2.32 +          val assign_update' = assign_update |> ok' ?
    2.33              (case opt_exec of
    2.34                SOME (eval, prints) =>
    2.35                  let
    2.36 @@ -420,12 +422,12 @@
    2.37                    | NONE => I)
    2.38                  end
    2.39              | NONE => I);
    2.40 -        in SOME (prev, same', flags', assign_update') end
    2.41 +        in SOME (prev, ok', flags', assign_update') end
    2.42        else NONE;
    2.43 -    val (common, same, flags, assign_update') =
    2.44 +    val (common, ok, flags, assign_update') =
    2.45        iterate_entries get_common node (NONE, true, (true, true), assign_update_empty);
    2.46      val (common', flags') =
    2.47 -      if same then
    2.48 +      if ok then
    2.49          let val last = Entries.get_after (get_entries node) common
    2.50          in (last, update_flags last flags) end
    2.51        else (common, flags);
    2.52 @@ -487,7 +489,7 @@
    2.53  
    2.54                      val (print_execs, common, (still_visible, initial)) =
    2.55                        if imports_result_changed then (assign_update_empty, NONE, (true, true))
    2.56 -                      else last_common state node0 node;
    2.57 +                      else last_common state node_required node0 node;
    2.58                      val common_command_exec = the_default_entry node common;
    2.59  
    2.60                      val (updated_execs, (command_id', (eval', _)), _) =

     3.1 --- a/src/Pure/PIDE/execution.ML	Mon Jul 29 22:17:32 2013 +0200
     3.2 +++ b/src/Pure/PIDE/execution.ML	Tue Jul 30 11:38:43 2013 +0200
     3.3 @@ -10,6 +10,7 @@
     3.4    val start: unit -> Document_ID.execution
     3.5    val discontinue: unit -> unit
     3.6    val is_running: Document_ID.execution -> bool
     3.7 +  val is_running_exec: Document_ID.exec -> bool
     3.8    val running: Document_ID.execution -> Document_ID.exec -> bool
     3.9    val cancel: Document_ID.exec -> unit
    3.10    val terminate: Document_ID.exec -> unit
    3.11 @@ -39,6 +40,9 @@
    3.12  
    3.13  (* registered execs *)
    3.14  
    3.15 +fun is_running_exec exec_id =
    3.16 +  Inttab.defined (snd (Synchronized.value state)) exec_id;
    3.17 +
    3.18  fun running execution_id exec_id =
    3.19    Synchronized.guarded_access state
    3.20      (fn (execution_id', execs) =>