1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 13:00:36 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 13:24:15 2013 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4    type eval
     1.5    val eval_eq: eval * eval -> bool
     1.6    val eval_result_state: eval -> Toplevel.state
     1.7 -  val eval_stable: eval -> bool
     1.8    val eval: (unit -> theory) -> Token.T list -> eval -> eval
     1.9    type print
    1.10    val print: bool -> string -> eval -> print list -> print list option
    1.11 @@ -28,7 +27,7 @@
    1.12  structure Command: COMMAND =
    1.13  struct
    1.14  
    1.15 -(** memo results -- including physical interrupts! **)
    1.16 +(** memo results -- including physical interrupts **)
    1.17  
    1.18  datatype 'a expr =
    1.19    Expr of Document_ID.exec * (unit -> 'a) |
    1.20 @@ -45,11 +44,6 @@
    1.21      Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    1.22    | Result res => Exn.release res);
    1.23  
    1.24 -fun memo_stable (Memo v) =
    1.25 -  (case Synchronized.value v of
    1.26 -   Expr _ => true
    1.27 - | Result res => not (Exn.is_interrupt_exn res));
    1.28 -
    1.29  fun memo_finished (Memo v) =
    1.30    (case Synchronized.value v of
    1.31     Expr _ => false
    1.32 @@ -125,9 +119,6 @@
    1.33  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.34  val eval_result_state = #state o eval_result;
    1.35  
    1.36 -fun eval_stable (Eval {exec_id, eval_process}) =
    1.37 -  Goal.stable_futures exec_id andalso memo_stable eval_process;
    1.38 -
    1.39  local
    1.40  
    1.41  fun run int tr st =
    1.42 @@ -220,11 +211,7 @@
    1.43  
    1.44  fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.45  
    1.46 -fun print_stable (Print {exec_id, print_process, ...}) =
    1.47 -  Goal.stable_futures exec_id andalso memo_stable print_process;
    1.48 -
    1.49 -fun print_finished (Print {exec_id, print_process, ...}) =
    1.50 -  Goal.stable_futures exec_id andalso memo_finished print_process;
    1.51 +fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
    1.52  
    1.53  fun print_persistent (Print {persistent, ...}) = persistent;
    1.54  
    1.55 @@ -264,8 +251,8 @@
    1.56        if command_visible then
    1.57          rev (Synchronized.value print_functions) |> map_filter (fn pr =>
    1.58            (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
    1.59 -            SOME print => if print_stable print then SOME print else new_print pr
    1.60 -          | NONE => new_print pr))
    1.61 +            NONE => new_print pr
    1.62 +          | some => some))
    1.63        else filter (fn print => print_finished print andalso print_persistent print) old_prints;
    1.64    in
    1.65      if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints