# HG changeset patch # User wenzelm # Date 1375117198 -7200 # Node ID e0169f13bd379eaa0afa5e10ab1aed027170f290 # Parent 627fb639a2d91556acc86e5db0b33ca61058068d 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; diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/Concurrent/future.ML --- 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" diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/PIDE/command.ML --- 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; diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/PIDE/document.ML --- 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 []; diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/PIDE/execution.ML --- 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); diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/PIDE/protocol.ML --- 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; diff -r 627fb639a2d9 -r e0169f13bd37 src/Pure/goal.ML --- 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);