1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 16:01:45 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 16:22:28 2013 +0200
     1.3 @@ -26,6 +26,13 @@
     1.4    type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
     1.5    val print: string -> eval -> print list
     1.6    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
     1.7 +  type exec = Document_ID.exec * (eval * print list)
     1.8 +  val no_exec: exec
     1.9 +  val exec_ids: exec -> Document_ID.exec list
    1.10 +  val exec_result: exec -> eval_state
    1.11 +  val exec_run: exec -> unit
    1.12 +  val stable_eval: exec -> bool
    1.13 +  val stable_print: print -> bool
    1.14  end;
    1.15  
    1.16  structure Command: COMMAND =
    1.17 @@ -80,6 +87,8 @@
    1.18  end;
    1.19  
    1.20  
    1.21 +(** main phases: read -- eval -- print **)
    1.22 +
    1.23  (* read *)
    1.24  
    1.25  fun read span =
    1.26 @@ -233,5 +242,35 @@
    1.27            (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
    1.28      in if do_print then Toplevel.print_state false st' else () end));
    1.29  
    1.30 +
    1.31 +
    1.32 +(** managed evaluation with potential interrupts **)
    1.33 +
    1.34 +(* execution *)
    1.35 +
    1.36 +type exec = Document_ID.exec * (eval * print list);
    1.37 +val no_exec: exec = (Document_ID.none, (no_eval, []));
    1.38 +
    1.39 +fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    1.40 +
    1.41 +fun exec_result ((_, (eval, _)): exec) = memo_result eval;
    1.42 +
    1.43 +fun exec_run ((_, (eval, prints)): exec) =
    1.44 + (memo_eval eval;
    1.45 +  prints |> List.app (fn {name, pri, print, ...} =>
    1.46 +    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    1.47 +
    1.48 +
    1.49 +(* stable situations *)
    1.50 +
    1.51 +fun stable_goals exec_id =
    1.52 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
    1.53 +
    1.54 +fun stable_eval ((exec_id, (eval, _)): exec) =
    1.55 +  stable_goals exec_id andalso memo_stable eval;
    1.56 +
    1.57 +fun stable_print ({exec_id, print, ...}: print) =
    1.58 +  stable_goals exec_id andalso memo_stable print;
    1.59 +
    1.60  end;
    1.61