1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 15 10:25:35 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 15 10:31:41 2013 +0200
     1.3 @@ -50,6 +50,11 @@
     1.4     Expr _ => true
     1.5   | Result res => not (Exn.is_interrupt_exn res));
     1.6  
     1.7 +fun memo_finished (Memo v) =
     1.8 +  (case Synchronized.value v of
     1.9 +   Expr _ => false
    1.10 + | Result res => not (Exn.is_interrupt_exn res));
    1.11 +
    1.12  fun memo_exec execution_id (Memo v) =
    1.13    Synchronized.guarded_access v
    1.14      (fn expr =>
    1.15 @@ -218,6 +223,9 @@
    1.16  fun print_stable (Print {exec_id, print_process, ...}) =
    1.17    Goal.stable_futures exec_id andalso memo_stable print_process;
    1.18  
    1.19 +fun print_finished (Print {exec_id, print_process, ...}) =
    1.20 +  Goal.stable_futures exec_id andalso memo_finished print_process;
    1.21 +
    1.22  fun print_persistent (Print {persistent, ...}) = persistent;
    1.23  
    1.24  in
    1.25 @@ -258,7 +266,7 @@
    1.26            (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
    1.27              SOME print => if print_stable print then SOME print else new_print pr
    1.28            | NONE => new_print pr))
    1.29 -      else filter (fn print => print_persistent print andalso print_stable print) old_prints;
    1.30 +      else filter (fn print => print_finished print andalso print_persistent print) old_prints;
    1.31    in
    1.32      if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
    1.33    end;