src/Pure/PIDE/command.ML
changeset 52532 c81d76f7f63d
parent 52530 99dd8b4ef3fe
child 52533 a95440dcd59c
--- a/src/Pure/PIDE/command.ML	Fri Jul 05 16:01:45 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 05 16:22:28 2013 +0200
@@ -26,6 +26,13 @@
   type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
   val print: string -> eval -> print list
   val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
+  type exec = Document_ID.exec * (eval * print list)
+  val no_exec: exec
+  val exec_ids: exec -> Document_ID.exec list
+  val exec_result: exec -> eval_state
+  val exec_run: exec -> unit
+  val stable_eval: exec -> bool
+  val stable_print: print -> bool
 end;
 
 structure Command: COMMAND =
@@ -80,6 +87,8 @@
 end;
 
 
+(** main phases: read -- eval -- print **)
+
 (* read *)
 
 fun read span =
@@ -233,5 +242,35 @@
           (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
     in if do_print then Toplevel.print_state false st' else () end));
 
+
+
+(** managed evaluation with potential interrupts **)
+
+(* execution *)
+
+type exec = Document_ID.exec * (eval * print list);
+val no_exec: exec = (Document_ID.none, (no_eval, []));
+
+fun exec_ids ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
+
+fun exec_result ((_, (eval, _)): exec) = memo_result eval;
+
+fun exec_run ((_, (eval, prints)): exec) =
+ (memo_eval eval;
+  prints |> List.app (fn {name, pri, print, ...} =>
+    memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
+
+
+(* stable situations *)
+
+fun stable_goals exec_id =
+  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
+
+fun stable_eval ((exec_id, (eval, _)): exec) =
+  stable_goals exec_id andalso memo_stable eval;
+
+fun stable_print ({exec_id, print, ...}: print) =
+  stable_goals exec_id andalso memo_stable print;
+
 end;