--- a/src/Pure/PIDE/command.ML Thu Jul 11 12:28:24 2013 +0200
+++ b/src/Pure/PIDE/command.ML Thu Jul 11 14:42:11 2013 +0200
@@ -9,6 +9,7 @@
type eval_process
type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
val eval_result_state: eval -> Toplevel.state
+ val eval_same: eval * eval -> bool
type print_process
type print =
{name: string, pri: int, persistent: bool,
@@ -16,9 +17,6 @@
type exec = eval * print list
val no_exec: exec
val exec_ids: exec option -> Document_ID.exec list
- val stable_eval: eval -> bool
- val stable_print: print -> bool
- val same_eval: eval * eval -> bool
val read: (unit -> theory) -> Token.T list -> Toplevel.transition
val eval: (unit -> theory) -> Token.T list -> eval -> eval
val print: bool -> string -> eval -> print list -> print list option
@@ -35,40 +33,42 @@
(** memo results -- including physical interrupts! **)
datatype 'a expr =
- Expr of unit -> 'a |
+ Expr of Document_ID.exec * (unit -> 'a) |
Result of 'a Exn.result;
abstype 'a memo = Memo of 'a expr Synchronized.var
with
-fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
+fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
-fun memo_eval (Memo v) =
- (case Synchronized.value v of
- Result res => res
- | _ =>
- Synchronized.guarded_access v
- (fn Result res => SOME (res, Result res)
- | Expr e =>
- let val res = Exn.capture e (); (*sic!*)
- in SOME (res, Result res) end))
- |> Exn.release;
-
-fun memo_fork params (Memo v) =
- (case Synchronized.value v of
- Result _ => ()
- | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
-
fun memo_result (Memo v) =
(case Synchronized.value v of
Result res => Exn.release res
| _ => raise Fail "Unfinished memo result");
-fun memo_stable (Memo v) =
+fun memo_exec (Memo v) =
(case Synchronized.value v of
- Expr _ => true
- | Result res => not (Exn.is_interrupt_exn res));
+ Result res => res
+ | _ =>
+ Synchronized.guarded_access v
+ (fn Result res => SOME (res, Result res)
+ | Expr (exec_id, e) =>
+ uninterruptible (fn restore_attributes => fn () =>
+ let
+ val _ = Exec.running exec_id;
+ val res = Exn.capture (restore_attributes e) ();
+ val _ =
+ if Exn.is_interrupt_exn res
+ then Exec.canceled exec_id
+ else Exec.finished exec_id;
+ in SOME (res, Result res) end) ()))
+ |> Exn.release;
+
+fun memo_fork params (Memo v) =
+ (case Synchronized.value v of
+ Result _ => ()
+ | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec (Memo v))));
end;
@@ -76,7 +76,7 @@
(** main phases of execution **)
-(* basic type definitions *)
+(* type definitions *)
type eval_state =
{failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
@@ -89,6 +89,9 @@
fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
val eval_result_state = #state o eval_result;
+fun eval_same ({exec_id, ...}: eval, {exec_id = exec_id', ...}: eval) =
+ exec_id = exec_id' andalso Exec.is_stable exec_id;
+
type print_process = unit memo;
type print =
{name: string, pri: int, persistent: bool,
@@ -101,21 +104,6 @@
| exec_ids (SOME ({exec_id, ...}, prints)) = exec_id :: map #exec_id prints;
-(* stable results *)
-
-fun stable_goals exec_id =
- not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
-
-fun stable_eval ({exec_id, eval_process}: eval) =
- stable_goals exec_id andalso memo_stable eval_process;
-
-fun stable_print ({exec_id, print_process, ...}: print) =
- stable_goals exec_id andalso memo_stable print_process;
-
-fun same_eval (eval: eval, eval': eval) =
- #exec_id eval = #exec_id eval' andalso stable_eval eval';
-
-
(* read *)
fun read init span =
@@ -208,7 +196,7 @@
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
(fn () => read init span |> Toplevel.exec_id exec_id) ();
in eval_state span tr (eval_result eval0) end;
- in {exec_id = exec_id, eval_process = memo process} end;
+ in {exec_id = exec_id, eval_process = memo exec_id process} end;
end;
@@ -226,6 +214,8 @@
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+fun print_stable (print: print) = Exec.is_stable (#exec_id print);
+
in
fun print command_visible command_name eval old_prints =
@@ -245,7 +235,7 @@
end;
in
{name = name, pri = pri, persistent = persistent,
- exec_id = exec_id, print_process = memo process}
+ exec_id = exec_id, print_process = memo exec_id process}
end;
in
(case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
@@ -258,9 +248,9 @@
if command_visible then
rev (Synchronized.value print_functions) |> map_filter (fn pr =>
(case find_first (equal (fst pr) o #name) old_prints of
- SOME print => if stable_print print then SOME print else new_print pr
+ SOME print => if print_stable print then SOME print else new_print pr
| NONE => new_print pr))
- else filter (fn print => #persistent print andalso stable_print print) old_prints;
+ else filter (fn print => #persistent print andalso print_stable print) old_prints;
in
if eq_list (op = o pairself #exec_id) (old_prints, new_prints) then NONE
else SOME new_prints
@@ -289,15 +279,15 @@
in if do_print then Toplevel.print_state false st' else () end));
-(* overall execution process *)
+(* combined execution process *)
fun run_print ({name, pri, print_process, ...}: print) =
(if Multithreading.enabled () then
memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
- else memo_eval) print_process;
+ else memo_exec) print_process;
fun execute (({eval_process, ...}, prints): exec) =
- (memo_eval eval_process; List.app run_print prints);
+ (memo_exec eval_process; List.app run_print prints);
end;
--- a/src/Pure/PIDE/document.ML Thu Jul 11 12:28:24 2013 +0200
+++ b/src/Pure/PIDE/document.ML Thu Jul 11 14:42:11 2013 +0200
@@ -421,7 +421,7 @@
val flags' = update_flags prev flags;
val same' =
(case (lookup_entry node0 command_id, opt_exec) of
- (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
+ (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval)
| _ => false);
val assign_update' = assign_update |> same' ?
(case opt_exec of
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/exec.ML Thu Jul 11 14:42:11 2013 +0200
@@ -0,0 +1,46 @@
+(* Title: Pure/PIDE/exec.ML
+ Author: Makarius
+
+Global management of command execution fragments.
+*)
+
+signature EXEC =
+sig
+ val is_stable: Document_ID.exec -> bool
+ val running: Document_ID.exec -> unit
+ val finished: Document_ID.exec -> unit
+ val canceled: Document_ID.exec -> unit
+ val purge_unstable: unit -> unit
+end;
+
+structure Exec: EXEC =
+struct
+
+val running_execs =
+ Synchronized.var "Exec.running_execs" (Inttab.empty: {stable: bool} Inttab.table);
+
+fun is_stable exec_id =
+ not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
+ (case Inttab.lookup (Synchronized.value running_execs) exec_id of
+ NONE => true
+ | SOME {stable} => stable);
+
+fun running exec_id =
+ Synchronized.change running_execs (Inttab.update_new (exec_id, {stable = true}));
+
+fun finished exec_id =
+ Synchronized.change running_execs (Inttab.delete exec_id);
+
+fun canceled exec_id =
+ Synchronized.change running_execs (Inttab.update (exec_id, {stable = false}));
+
+fun purge_unstable () =
+ Synchronized.guarded_access running_execs
+ (fn tab =>
+ let
+ val unstable = Inttab.fold (fn (exec_id, {stable = false}) => cons exec_id | _ => I) tab [];
+ val tab' = fold Inttab.delete unstable tab;
+ in SOME ((), tab') end);
+
+end;
+
--- a/src/Pure/PIDE/protocol.ML Thu Jul 11 12:28:24 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu Jul 11 14:42:11 2013 +0200
@@ -60,6 +60,7 @@
|> YXML.string_of_body);
val _ = List.app Future.cancel_group (Goal.reset_futures ());
+ val _ = Exec.purge_unstable ();
val _ = Isabelle_Process.reset_tracing ();
val _ =
Event_Timer.request (Time.+ (Time.now (), seconds 0.02))
--- a/src/Pure/ROOT Thu Jul 11 12:28:24 2013 +0200
+++ b/src/Pure/ROOT Thu Jul 11 14:42:11 2013 +0200
@@ -150,6 +150,7 @@
"ML/ml_syntax.ML"
"ML/ml_thms.ML"
"PIDE/active.ML"
+ "PIDE/exec.ML"
"PIDE/command.ML"
"PIDE/document.ML"
"PIDE/document_id.ML"
--- a/src/Pure/ROOT.ML Thu Jul 11 12:28:24 2013 +0200
+++ b/src/Pure/ROOT.ML Thu Jul 11 14:42:11 2013 +0200
@@ -267,6 +267,7 @@
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
use "Thy/present.ML";
+use "PIDE/exec.ML";
use "PIDE/command.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";