diff --git a/src/Pure/Concurrent/lazy.ML b/src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML
+++ b/src/Pure/Concurrent/lazy.ML
@@ -1,115 +1,105 @@
 (*  Title:      Pure/Concurrent/lazy.ML
     Author:     Makarius
 
 Lazy evaluation with memoing of results and regular exceptions.
 Parallel version based on (passive) futures, to avoid critical or
 multiple evaluation (unless interrupted).
 *)
 
 signature LAZY =
 sig
   type 'a lazy
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
   val is_running: 'a lazy -> bool
   val is_finished: 'a lazy -> bool
-  val finished_result: 'a lazy -> 'a Exn.result option
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   val future: Future.params -> 'a lazy -> 'a future
 end;
 
 structure Lazy: LAZY =
 struct
 
 (* datatype *)
 
 datatype 'a expr =
   Expr of unit -> 'a |
   Result of 'a future;
 
 abstype 'a lazy = Lazy of 'a expr Synchronized.var
 with
 
 fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
 fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
 
 fun peek (Lazy var) =
   (case Synchronized.value var of
     Expr _ => NONE
   | Result res => Future.peek res);
 
 
 (* status *)
 
 fun is_future pred (Lazy var) =
   (case Synchronized.value var of
     Expr _ => false
   | Result res => pred res);
 
 fun is_running x = is_future (not o Future.is_finished) x;
 
 fun is_finished x =
   is_future (fn res =>
     Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
 
-fun finished_result (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => NONE
-  | Result res =>
-      if Future.is_finished res then
-        let val result = Future.join_result res
-        in if Exn.is_interrupt_exn result then NONE else SOME result end
-      else NONE);
-
 
 (* force result *)
 
 fun force_result (Lazy var) =
   (case peek (Lazy var) of
     SOME res => res
   | NONE =>
       uninterruptible (fn restore_attributes => fn () =>
         let
           val (expr, x) =
             Synchronized.change_result var
               (fn Expr e =>
                     let val x = Future.promise I
                     in ((SOME e, x), Result x) end
                 | Result x => ((NONE, x), Result x));
         in
           (case expr of
             SOME e =>
               let
                 val res0 = Exn.capture (restore_attributes e) ();
                 val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
                 val res = Future.join_result x;
                 (*semantic race: some other threads might see the same
                   interrupt, until there is a fresh start*)
                 val _ =
                   if Exn.is_interrupt_exn res then
                     Synchronized.change var (fn _ => Expr e)
                   else ();
               in res end
           | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
         end) ());
 
 
 end;
 
 fun force r = Exn.release (force_result r);
 fun map f x = lazy (fn () => f (force x));
 
 
 (* future evaluation *)
 
 fun future params x =
   if is_finished x then Future.value_result (force_result x)
   else (singleton o Future.forks) params (fn () => force x);
 
 end;
 
 type 'a lazy = 'a Lazy.lazy;
 
diff --git a/src/Pure/PIDE/command.ML b/src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML
+++ b/src/Pure/PIDE/command.ML
@@ -1,414 +1,410 @@
 (*  Title:      Pure/PIDE/command.ML
     Author:     Makarius
 
 Prover command execution: read -- eval -- print.
 *)
 
 signature COMMAND =
 sig
   type blob = (string * (SHA1.digest * string list) option) Exn.result
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
   val read_thy: Toplevel.state -> theory
   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     blob list -> Token.T list -> Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     blob list -> Token.T list -> eval -> eval
   type print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print_function =
     {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
   val print_function: string -> print_function -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
   val no_exec: exec
   val exec_ids: exec option -> Document_ID.exec list
   val exec: Document_ID.execution -> exec -> unit
 end;
 
 structure Command: COMMAND =
 struct
 
 (** main phases of execution **)
 
 (* read *)
 
 type blob =
   (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
 
 fun read_file_node file_node master_dir pos src_path =
   let
     val _ = Position.report pos Markup.language_path;
     val _ =
       (case try Url.explode file_node of
         NONE => ()
       | SOME (Url.File _) => ()
       | _ =>
          (Position.report pos (Markup.path file_node);
           error ("Prover cannot load remote file " ^
             Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
     val full_path = File.check_file (File.full_path master_dir src_path);
     val _ = Position.report pos (Markup.path (Path.implode full_path));
     val text = File.read full_path;
     val lines = split_lines text;
     val digest = SHA1.digest text;
   in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
 
 val read_file = read_file_node "";
 
 local
 
 fun blob_file src_path lines digest file_node =
   let
     val file_pos =
       Position.file file_node |>
       (case Position.get_id (Position.thread_data ()) of
         NONE => I
       | SOME exec_id => Position.put_id exec_id);
   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
 
 fun resolve_files keywords master_dir blobs toks =
   (case Outer_Syntax.parse_spans toks of
     [span] => span
       |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
         let
           fun make_file src_path (Exn.Res (file_node, NONE)) =
                 Exn.interruptible_capture (fn () =>
                   read_file_node file_node master_dir pos src_path) ()
             | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
                (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
                 Exn.Res (blob_file src_path lines digest file_node))
             | make_file _ (Exn.Exn e) = Exn.Exn e;
           val src_paths = Keyword.command_files keywords cmd path;
         in
           if null blobs then
             map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
           else if length src_paths = length blobs then
             map2 make_file src_paths blobs
           else error ("Misalignment of inlined files" ^ Position.here pos)
         end)
       |> Command_Span.content
   | _ => toks);
 
 val bootstrap_thy = ML_Context.the_global_context ();
 
 in
 
 fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
 
 fun read keywords thy master_dir init blobs span =
   let
     val command_reports = Outer_Syntax.command_reports thy;
 
     val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.pos_of tok
       | NONE => #1 proper_range);
 
     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
     val _ = Position.reports_text (token_reports @ maps command_reports span);
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
       (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
         [tr] => Toplevel.modify_init init tr
       | [] => Toplevel.ignored (#1 (Token.range_of span))
       | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
       handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
   end;
 
 end;
 
 
 (* eval *)
 
 type eval_state =
   {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
 val init_eval_state =
   {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
 
 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
 
 fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
 val eval_eq = op = o apply2 eval_exec_id;
 
 val eval_running = Execution.is_running_exec o eval_exec_id;
 fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
 
-fun eval_result (Eval {exec_id, eval_process}) =
-  (case Lazy.finished_result eval_process of
-    SOME result => Exn.release result
-  | NONE => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
-
+fun eval_result (Eval {eval_process, ...}) = Lazy.force eval_process;
 val eval_result_state = #state o eval_result;
 
 local
 
 fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () =>
   let
     val name = Toplevel.name_of tr;
     val res =
       if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
       else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
       else NONE;
   in
     (case res of
       NONE => st0
     | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
   end) ();
 
 fun run keywords int tr st =
   if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
 
 fun check_cmts span tr st' =
   Toplevel.setmp_thread_position tr
     (fn () =>
       Outer_Syntax.side_comments span |> maps (fn cmt =>
         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
           handle exn =>
             if Exn.is_interrupt exn then reraise exn
             else Runtime.exn_messages_ids exn)) ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
 
 fun status tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
 
 fun proof_status tr st =
   (case try Toplevel.proof_of st of
     SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
 fun eval_state keywords span tr ({malformed, state, ...}: eval_state) =
   if malformed then
     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   else
     let
       val _ = Multithreading.interrupted ();
 
       val malformed' = Toplevel.is_malformed tr;
       val st = reset_state keywords tr state;
 
       val _ = status tr Markup.running;
       val (errs1, result) = run keywords true tr st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
       val errs = errs1 @ errs2;
       val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
     in
       (case result of
         NONE =>
           let
             val _ = status tr Markup.failed;
             val _ = status tr Markup.finished;
             val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
           in {failed = true, malformed = malformed', command = tr, state = st} end
       | SOME st' =>
           let
             val _ = proof_status tr st';
             val _ = status tr Markup.finished;
           in {failed = false, malformed = malformed', command = tr, state = st'} end)
     end;
 
 in
 
 fun eval keywords master_dir init blobs span eval0 =
   let
     val exec_id = Document_ID.make ();
     fun process () =
       let
         val eval_state0 = eval_result eval0;
         val thy = read_thy (#state eval_state0);
         val tr =
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
             (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
       in eval_state keywords span tr eval_state0 end;
   in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
 
 end;
 
 
 (* print *)
 
 datatype print = Print of
  {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   exec_id: Document_ID.exec, print_process: unit lazy};
 
 fun print_exec_id (Print {exec_id, ...}) = exec_id;
 val print_eq = op = o apply2 print_exec_id;
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
   {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
     {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
 
 local
 
 val print_functions =
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr opt_context e =
   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
     handle exn =>
       if Exn.is_interrupt exn then reraise exn
       else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
 
 fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
 val overlay_ord = prod_ord string_ord (list_ord string_ord);
 
 in
 
 fun print command_visible command_overlays keywords command_name eval old_prints =
   let
     val print_functions = Synchronized.value print_functions;
 
     fun make_print name args {delay, pri, persistent, strict, print_fn} =
       let
         val exec_id = Document_ID.make ();
         fun process () =
           let
             val {failed, command, state = st', ...} = eval_result eval;
             val tr = Toplevel.exec_id exec_id command;
             val opt_context = try Toplevel.generic_theory_of st';
           in
             if failed andalso strict then ()
             else print_error tr opt_context (fn () => print_fn tr st')
           end;
       in
         Print {
           name = name, args = args, delay = delay, pri = pri, persistent = persistent,
           exec_id = exec_id, print_process = Lazy.lazy process}
       end;
 
     fun bad_print name args exn =
       make_print name args {delay = NONE, pri = 0, persistent = false,
         strict = false, print_fn = fn _ => fn _ => reraise exn};
 
     fun new_print name args get_pr =
       let
         val params =
          {keywords = keywords,
           command_name = command_name,
           args = args,
           exec_id = eval_exec_id eval};
       in
         (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print name args pr)
         | Exn.Exn exn => SOME (bad_print name args exn))
       end;
 
     fun get_print (a, b) =
       (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
         NONE =>
           (case AList.lookup (op =) print_functions a of
             NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a)))
           | SOME get_pr => new_print a b get_pr)
       | some => some);
 
     val new_prints =
       if command_visible then
         fold (fn (a, _) => cons (a, [])) print_functions command_overlays
         |> sort_distinct overlay_ord
         |> map_filter get_print
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   end;
 
 fun print_function name f =
   Synchronized.change print_functions (fn funs =>
    (if not (AList.defined (op =) funs name) then ()
     else warning ("Redefining command print function: " ^ quote name);
     AList.update (op =) (name, f) funs));
 
 fun no_print_function name =
   Synchronized.change print_functions (filter_out (equal name o #1));
 
 end;
 
 val _ =
   print_function "Execution.print"
     (fn {args, exec_id, ...} =>
       if null args then
         SOME {delay = NONE, pri = 1, persistent = false, strict = false,
           print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
       else NONE);
 
 val _ =
   print_function "print_state"
     (fn {keywords, command_name, ...} =>
       if Keyword.is_printed keywords command_name then
         SOME {delay = NONE, pri = 1, persistent = false, strict = false,
           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
       else NONE);
 
 
 (* combined execution *)
 
 type exec = eval * print list;
 val no_exec: exec =
   (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []);
 
 fun exec_ids NONE = []
   | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
 
 local
 
 fun run_process execution_id exec_id process =
   let val group = Future.worker_subgroup () in
     if Execution.running execution_id exec_id [group] then
       ignore (Future.task_context "Command.run_process" group Lazy.force_result process)
     else ()
   end;
 
 fun ignore_process process =
   Lazy.is_running process orelse Lazy.is_finished process;
 
 fun run_eval execution_id (Eval {exec_id, eval_process}) =
   if Lazy.is_finished eval_process then ()
   else run_process execution_id exec_id eval_process;
 
 fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
   if ignore_process print_process then ()
   else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
   then
     let
       val group = Future.worker_subgroup ();
       fun fork () =
         ignore ((singleton o Future.forks)
           {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
           (fn () =>
             if ignore_process print_process then ()
             else run_process execution_id exec_id print_process));
     in
       (case delay of
         NONE => fork ()
       | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
     end
   else run_process execution_id exec_id print_process;
 
 in
 
 fun exec execution_id (eval, prints) =
   (run_eval execution_id eval; List.app (run_print execution_id) prints);
 
 end;
 
 end;
 
diff --git a/src/Pure/PIDE/execution.ML b/src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML
+++ b/src/Pure/PIDE/execution.ML
@@ -1,188 +1,183 @@
 (*  Title:      Pure/PIDE/execution.ML
     Author:     Makarius
 
 Global management of execution.  Unique running execution serves as
 barrier for further exploration of forked command execs.
 *)
 
 signature EXECUTION =
 sig
   val start: unit -> Document_ID.execution
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
   val is_running_exec: Document_ID.exec -> bool
   val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
   val peek: Document_ID.exec -> Future.group list
   val cancel: Document_ID.exec -> unit
   val terminate: Document_ID.exec -> unit
   type params = {name: string, pos: Position.T, pri: int}
   val fork: params -> (unit -> 'a) -> 'a future
   val print: params -> (unit -> unit) -> unit
   val fork_prints: Document_ID.exec -> unit
   val purge: Document_ID.exec list -> unit
   val reset: unit -> Future.group list
   val shutdown: unit -> unit
 end;
 
 structure Execution: EXECUTION =
 struct
 
 (* global state *)
 
 type print = {name: string, pri: int, body: unit -> unit};
 type exec_state = Future.group list * print list;  (*active forks, prints*)
 type state =
   Document_ID.execution * (*overall document execution*)
   exec_state Inttab.table;  (*running command execs*)
 
 val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
 val state = Synchronized.var "Execution.state" init_state;
 
 fun get_state () = Synchronized.value state;
 fun change_state_result f = Synchronized.change_result state f;
 fun change_state f = Synchronized.change state f;
 
 fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
 
 
 (* unique running execution *)
 
 fun start () =
   let
     val execution_id = Document_ID.make ();
     val _ = change_state (apfst (K execution_id));
   in execution_id end;
 
 fun discontinue () = change_state (apfst (K Document_ID.none));
 
 fun is_running execution_id = execution_id = #1 (get_state ());
 
 
 (* execs *)
 
 fun is_running_exec exec_id =
   Inttab.defined (#2 (get_state ())) exec_id;
 
 fun running execution_id exec_id groups =
   change_state_result (fn (execution_id', execs) =>
     let
-      val continue = execution_id = execution_id';
-      val execs' =
-        if continue then
-          Inttab.update_new (exec_id, (groups, [])) execs
-            handle Inttab.DUP dup =>
-              raise Fail ("Execution already registered: " ^ Document_ID.print dup)
-        else execs;
-    in (continue, (execution_id', execs')) end);
+      val ok = execution_id = execution_id' andalso not (Inttab.defined execs exec_id);
+      val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
+    in (ok, (execution_id', execs')) end);
 
 fun peek exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of
     SOME (groups, _) => groups
   | NONE => []);
 
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
 fun terminate exec_id = List.app Future.terminate (peek exec_id);
 
 
 (* fork *)
 
 fun status task markups =
   let
     val props =
       if ! Multithreading.trace >= 2
       then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
   in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
 
 type params = {name: string, pos: Position.T, pri: int};
 
 fun fork ({name, pos, pri}: params) e =
   uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
     let
       val exec_id = the_default 0 (Position.parse_id pos);
       val group = Future.worker_subgroup ();
       val _ = change_state (apsnd (fn execs =>
         (case Inttab.lookup execs exec_id of
           SOME (groups, prints) =>
             Inttab.update (exec_id, (group :: groups, prints)) execs
         | NONE => raise Fail (unregistered exec_id))));
 
       val future =
         (singleton o Future.forks)
           {name = name, group = SOME group, deps = [], pri = pri, interrupts = false}
           (fn () =>
             let
               val task = the (Future.worker_task ());
               val _ = status task [Markup.running];
               val result =
                 Exn.capture (Future.interruptible_task e) ()
                 |> Future.identify_result pos;
               val _ = status task [Markup.joined];
               val _ =
                 (case result of
                   Exn.Exn exn =>
                    (status task [Markup.failed];
                     status task [Markup.finished];
                     Output.report [Markup.markup_only Markup.bad];
                     if exec_id = 0 then ()
                     else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
                 | Exn.Res _ =>
                     status task [Markup.finished])
             in Exn.release result end);
 
       val _ = status (Future.task_of future) [Markup.forked];
     in future end)) ();
 
 
 (* print *)
 
 fun print ({name, pos, pri}: params) e =
   change_state (apsnd (fn execs =>
     let
       val exec_id = the_default 0 (Position.parse_id pos);
       val print = {name = name, pri = pri, body = e};
     in
       (case Inttab.lookup execs exec_id of
         SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs
       | NONE => raise Fail (unregistered exec_id))
     end));
 
 fun fork_prints exec_id =
   (case Inttab.lookup (#2 (get_state ())) exec_id of
     SOME (_, prints) =>
       if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
       then List.app (fn {body, ...} => body ()) (rev prints)
       else
         let val pos = Position.thread_data () in
           List.app (fn {name, pri, body} =>
             ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
         end
   | NONE => raise Fail (unregistered exec_id));
 
 
 (* cleanup *)
 
 fun purge exec_ids =
   (change_state o apsnd) (fn execs =>
     let
       val execs' = fold Inttab.delete_safe exec_ids execs;
       val () =
         (execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () =>
           if Inttab.defined execs' exec_id then ()
           else groups |> List.app (fn group =>
             if Task_Queue.is_canceled group then ()
             else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
     in execs' end);
 
 fun reset () =
   change_state_result (fn (_, execs) =>
     let val groups = Inttab.fold (append o #1 o #2) execs []
     in (groups, init_state) end);
 
 fun shutdown () =
   (Future.shutdown ();
     (case maps Task_Queue.group_status (reset ()) of
       [] => ()
     | exns => raise Par_Exn.make exns));
 
 end;