src/Pure/PIDE/command.ML
changeset 52761 909167fdd367
parent 52713 cd3ce844248f
child 52762 c2a6e220f157
--- a/src/Pure/PIDE/command.ML	Mon Jul 29 13:00:36 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 29 13:24:15 2013 +0200
@@ -10,7 +10,6 @@
   type eval
   val eval_eq: eval * eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval_stable: eval -> bool
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   type print
   val print: bool -> string -> eval -> print list -> print list option
@@ -28,7 +27,7 @@
 structure Command: COMMAND =
 struct
 
-(** memo results -- including physical interrupts! **)
+(** memo results -- including physical interrupts **)
 
 datatype 'a expr =
   Expr of Document_ID.exec * (unit -> 'a) |
@@ -45,11 +44,6 @@
     Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
   | Result res => Exn.release res);
 
-fun memo_stable (Memo v) =
-  (case Synchronized.value v of
-   Expr _ => true
- | Result res => not (Exn.is_interrupt_exn res));
-
 fun memo_finished (Memo v) =
   (case Synchronized.value v of
    Expr _ => false
@@ -125,9 +119,6 @@
 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
 val eval_result_state = #state o eval_result;
 
-fun eval_stable (Eval {exec_id, eval_process}) =
-  Goal.stable_futures exec_id andalso memo_stable eval_process;
-
 local
 
 fun run int tr st =
@@ -220,11 +211,7 @@
 
 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
 
-fun print_stable (Print {exec_id, print_process, ...}) =
-  Goal.stable_futures exec_id andalso memo_stable print_process;
-
-fun print_finished (Print {exec_id, print_process, ...}) =
-  Goal.stable_futures exec_id andalso memo_finished print_process;
+fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
@@ -264,8 +251,8 @@
       if command_visible then
         rev (Synchronized.value print_functions) |> map_filter (fn pr =>
           (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
-            SOME print => if print_stable print then SOME print else new_print pr
-          | NONE => new_print pr))
+            NONE => new_print pr
+          | some => some))
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints