1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 16:22:28 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 17:09:28 2013 +0200
     1.3 @@ -19,19 +19,20 @@
     1.4    val read: span -> Toplevel.transition
     1.5    type eval_state =
     1.6      {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
     1.7 -  type eval = eval_state memo
     1.8 +  type eval = {exec_id: Document_ID.exec, eval: eval_state memo}
     1.9    val no_eval: eval
    1.10 +  val eval_result: eval -> eval_state
    1.11    val eval: span -> Toplevel.transition -> eval_state -> eval_state
    1.12    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.13    type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
    1.14    val print: string -> eval -> print list
    1.15    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.16 -  type exec = Document_ID.exec * (eval * print list)
    1.17 +  type exec = eval * print list
    1.18    val no_exec: exec
    1.19    val exec_ids: exec -> Document_ID.exec list
    1.20    val exec_result: exec -> eval_state
    1.21    val exec_run: exec -> unit
    1.22 -  val stable_eval: exec -> bool
    1.23 +  val stable_eval: eval -> bool
    1.24    val stable_print: print -> bool
    1.25  end;
    1.26  
    1.27 @@ -125,8 +126,10 @@
    1.28  val no_eval_state: eval_state =
    1.29    {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    1.30  
    1.31 -type eval = eval_state memo;
    1.32 -val no_eval = memo_value no_eval_state;
    1.33 +type eval = {exec_id: Document_ID.exec, eval: eval_state memo};
    1.34 +
    1.35 +val no_eval: eval = {exec_id = Document_ID.none, eval = memo_value no_eval_state};
    1.36 +fun eval_result ({eval, ...}: eval) = memo_result eval;
    1.37  
    1.38  local
    1.39  
    1.40 @@ -210,7 +213,7 @@
    1.41            val exec_id = Document_ID.make ();
    1.42            fun body () =
    1.43              let
    1.44 -              val {failed, command, state = st', ...} = memo_result eval;
    1.45 +              val {failed, command, state = st', ...} = eval_result eval;
    1.46                val tr = Toplevel.put_id exec_id command;
    1.47              in if failed then () else print_error tr (fn () => print_fn tr st') () end;
    1.48          in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
    1.49 @@ -219,7 +222,7 @@
    1.50            val exec_id = Document_ID.make ();
    1.51            fun body () =
    1.52              let
    1.53 -              val {command, ...} = memo_result eval;
    1.54 +              val {command, ...} = eval_result eval;
    1.55                val tr = Toplevel.put_id exec_id command;
    1.56              in output_error tr exn end;
    1.57          in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
    1.58 @@ -244,29 +247,29 @@
    1.59  
    1.60  
    1.61  
    1.62 -(** managed evaluation with potential interrupts **)
    1.63 +(** managed evaluation **)
    1.64  
    1.65  (* execution *)
    1.66  
    1.67 -type exec = Document_ID.exec * (eval * print list);
    1.68 -val no_exec: exec = (Document_ID.none, (no_eval, []));
    1.69 +type exec = eval * print list;
    1.70 +val no_exec: exec = (no_eval, []);
    1.71  
    1.72 -fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    1.73 +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
    1.74  
    1.75 -fun exec_result ((_, (eval, _)): exec) = memo_result eval;
    1.76 +fun exec_result (({eval, ...}, _): exec) = memo_result eval;
    1.77  
    1.78 -fun exec_run ((_, (eval, prints)): exec) =
    1.79 +fun exec_run (({eval, ...}, prints): exec) =
    1.80   (memo_eval eval;
    1.81    prints |> List.app (fn {name, pri, print, ...} =>
    1.82      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    1.83  
    1.84  
    1.85 -(* stable situations *)
    1.86 +(* stable situations after cancellation *)
    1.87  
    1.88  fun stable_goals exec_id =
    1.89    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    1.90  
    1.91 -fun stable_eval ((exec_id, (eval, _)): exec) =
    1.92 +fun stable_eval ({exec_id, eval}: eval) =
    1.93    stable_goals exec_id andalso memo_stable eval;
    1.94  
    1.95  fun stable_print ({exec_id, print, ...}: print) =