keep memo_exec execution running, which is important to cancel goal forks eventually;
run as nested worker task to keep main group valid, even after cancelation of removed subgroups;
do not memoize interrupt, but absorb it silently in main execution;
Goal.purge_futures: rough sanity check of group status;
--- a/src/Pure/Concurrent/future.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Jul 29 18:59:58 2013 +0200
@@ -48,6 +48,7 @@
val worker_group: unit -> group option
val the_worker_group: unit -> group
val worker_subgroup: unit -> group
+ val worker_nest: string -> ('a -> 'b) -> 'a -> 'b
val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b
type 'a future
val task_of: 'a future -> task
@@ -108,6 +109,9 @@
fun worker_subgroup () = new_group (worker_group ());
+fun worker_nest name f x =
+ setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x;
+
fun worker_guest name group f x =
if is_some (worker_task ()) then
raise Fail "Already running as worker thread"
--- a/src/Pure/PIDE/command.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/PIDE/command.ML Mon Jul 29 18:59:58 2013 +0200
@@ -28,7 +28,7 @@
structure Command: COMMAND =
struct
-(** memo results -- including physical interrupts **)
+(** memo results **)
datatype 'a expr =
Expr of Document_ID.exec * (unit -> 'a) |
@@ -48,24 +48,25 @@
fun memo_finished (Memo v) =
(case Synchronized.value v of
Expr _ => false
- | Result res => not (Exn.is_interrupt_exn res));
+ | Result _ => true);
fun memo_exec execution_id (Memo v) =
Synchronized.timed_access v (K (SOME Time.zeroTime))
(fn expr =>
(case expr of
- Expr (exec_id, e) =>
+ Expr (exec_id, body) =>
uninterruptible (fn restore_attributes => fn () =>
if Execution.running execution_id exec_id then
let
- val res = Exn.capture (restore_attributes e) ();
- val _ = Execution.finished exec_id;
- in SOME (Exn.is_interrupt_exn res, Result res) end
- else SOME (true, expr)) ()
- | Result _ => SOME (false, expr)))
- |> (fn SOME false => ()
- | SOME true => Exn.interrupt ()
- | NONE => error "Conflicting command execution");
+ val res =
+ (body
+ |> restore_attributes
+ |> Future.worker_nest "Command.memo_exec"
+ |> Exn.interruptible_capture) ();
+ in SOME ((), Result res) end
+ else SOME ((), expr)) ()
+ | Result _ => SOME ((), expr)))
+ |> (fn NONE => error "Conflicting command execution" | _ => ());
fun memo_fork params execution_id (Memo v) =
(case Synchronized.value v of
@@ -216,7 +217,7 @@
fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
-fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
+fun print_finished (Print {print_process, ...}) = memo_finished print_process;
fun print_persistent (Print {persistent, ...}) = persistent;
--- a/src/Pure/PIDE/document.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/PIDE/document.ML Mon Jul 29 18:59:58 2013 +0200
@@ -303,19 +303,20 @@
if visible_node node orelse pending_result node then
let
val former_task = Symtab.lookup frontier name;
+ fun body () =
+ iterate_entries (fn (_, opt_exec) => fn () =>
+ (case opt_exec of
+ SOME exec =>
+ if Execution.is_running execution_id
+ then SOME (Command.exec execution_id exec)
+ else NONE
+ | NONE => NONE)) node ()
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
val future =
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group NONE),
deps = the_list former_task @ map #2 (maps #2 deps),
- pri = pri, interrupts = false}
- (fn () =>
- iterate_entries (fn (_, opt_exec) => fn () =>
- (case opt_exec of
- SOME exec =>
- if Execution.is_running execution_id
- then SOME (Command.exec execution_id exec)
- else NONE
- | NONE => NONE)) node ());
+ pri = pri, interrupts = false} body;
in [(name, Future.task_of future)] end
else [])
else [];
--- a/src/Pure/PIDE/execution.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/PIDE/execution.ML Mon Jul 29 18:59:58 2013 +0200
@@ -11,7 +11,6 @@
val discontinue: unit -> unit
val is_running: Document_ID.execution -> bool
val running: Document_ID.execution -> Document_ID.exec -> bool
- val finished: Document_ID.exec -> unit
val cancel: Document_ID.exec -> unit
val terminate: Document_ID.exec -> unit
end;
@@ -52,12 +51,6 @@
else execs;
in SOME (continue, (execution_id', execs')) end);
-fun finished exec_id =
- Synchronized.change state
- (apsnd (fn execs =>
- Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
- error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
-
fun peek_list exec_id =
the_list (Inttab.lookup (snd (Synchronized.value state)) exec_id);
--- a/src/Pure/PIDE/protocol.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Jul 29 18:59:58 2013 +0200
@@ -75,7 +75,7 @@
Isabelle_Process.protocol_command "Document.dialog_result"
(fn [serial, result] =>
Active.dialog_result (Markup.parse_int serial) result
- handle exn => if Exn.is_interrupt exn then () else reraise exn);
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
end;
--- a/src/Pure/goal.ML Mon Jul 29 16:52:04 2013 +0200
+++ b/src/Pure/goal.ML Mon Jul 29 18:59:58 2013 +0200
@@ -181,11 +181,18 @@
fun peek_futures id =
map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
+fun check_canceled id group =
+ if Task_Queue.is_canceled group then ()
+ else raise Fail ("Attempt to purge valid execution " ^ string_of_int id);
+
fun purge_futures ids =
Synchronized.change forked_proofs (fn (_, tab) =>
let
val tab' = fold Inttab.delete_safe ids tab;
- val n' = Inttab.fold (Integer.add o length o #2) tab' 0;
+ val n' =
+ Inttab.fold (fn (id, futures) => fn m =>
+ if Inttab.defined tab' id then m + length futures
+ else (List.app (check_canceled id o #1) futures; m)) tab 0;
val _ = Future.forked_proofs := n';
in (n', tab') end);