1.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 22:17:32 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Jul 30 11:38:43 2013 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4    is_some (Thy_Info.lookup_theory name) orelse
     1.5    can get_header node andalso (not full orelse is_some (get_result node));
     1.6  
     1.7 -fun last_common state node0 node =
     1.8 +fun last_common state node_required node0 node =
     1.9    let
    1.10      fun update_flags prev (visible, initial) =
    1.11        let
    1.12 @@ -400,15 +400,17 @@
    1.13            | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
    1.14        in (visible', initial') end;
    1.15  
    1.16 -    fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) =
    1.17 -      if same then
    1.18 +    fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
    1.19 +      if ok then
    1.20          let
    1.21 -          val flags' = update_flags prev flags;
    1.22 -          val same' =
    1.23 +          val flags' as (visible', _) = update_flags prev flags;
    1.24 +          val ok' =
    1.25              (case (lookup_entry node0 command_id, opt_exec) of
    1.26 -              (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
    1.27 +              (SOME (eval0, _), SOME (eval, _)) =>
    1.28 +                Command.eval_eq (eval0, eval) andalso
    1.29 +                  (visible' orelse node_required orelse Command.eval_running eval)
    1.30              | _ => false);
    1.31 -          val assign_update' = assign_update |> same' ?
    1.32 +          val assign_update' = assign_update |> ok' ?
    1.33              (case opt_exec of
    1.34                SOME (eval, prints) =>
    1.35                  let
    1.36 @@ -420,12 +422,12 @@
    1.37                    | NONE => I)
    1.38                  end
    1.39              | NONE => I);
    1.40 -        in SOME (prev, same', flags', assign_update') end
    1.41 +        in SOME (prev, ok', flags', assign_update') end
    1.42        else NONE;
    1.43 -    val (common, same, flags, assign_update') =
    1.44 +    val (common, ok, flags, assign_update') =
    1.45        iterate_entries get_common node (NONE, true, (true, true), assign_update_empty);
    1.46      val (common', flags') =
    1.47 -      if same then
    1.48 +      if ok then
    1.49          let val last = Entries.get_after (get_entries node) common
    1.50          in (last, update_flags last flags) end
    1.51        else (common, flags);
    1.52 @@ -487,7 +489,7 @@
    1.53  
    1.54                      val (print_execs, common, (still_visible, initial)) =
    1.55                        if imports_result_changed then (assign_update_empty, NONE, (true, true))
    1.56 -                      else last_common state node0 node;
    1.57 +                      else last_common state node_required node0 node;
    1.58                      val common_command_exec = the_default_entry node common;
    1.59  
    1.60                      val (updated_execs, (command_id', (eval', _)), _) =