diff --git a/src/Pure/Concurrent/future.ML b/src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML
+++ b/src/Pure/Concurrent/future.ML
@@ -1,715 +1,715 @@
 (*  Title:      Pure/Concurrent/future.ML
     Author:     Makarius
 
 Value-oriented parallel execution via futures and promises.
 *)
 
 signature FUTURE =
 sig
   type task = Task_Queue.task
   type group = Task_Queue.group
   val new_group: group option -> group
   val worker_task: unit -> task option
   val worker_group: unit -> group option
   val the_worker_group: unit -> group
   val worker_subgroup: unit -> group
   type 'a future
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
   val error_message: Position.T -> (serial * string) * string option -> unit
   val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
   type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
   val default_params: params
   val forks: params -> (unit -> 'a) list -> 'a future list
   val fork: (unit -> 'a) -> 'a future
   val get_result: 'a future -> 'a Exn.result
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
   val forked_results: {name: string, deps: Task_Queue.task list} ->
     (unit -> 'a) list -> 'a Exn.result list
   val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b
   val enabled: unit -> bool
   val relevant: 'a list -> bool
   val proofs_enabled: int -> bool
   val proofs_enabled_timing: Time.time -> bool
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val cond_forks: params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
   val promise_name: string -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
   val snapshot: group list -> task list
   val shutdown: unit -> unit
 end;
 
 structure Future: FUTURE =
 struct
 
 (** future values **)
 
 type task = Task_Queue.task;
 type group = Task_Queue.group;
 val new_group = Task_Queue.new_group;
 
 
 (* identifiers *)
 
 local
   val worker_task_var = Thread_Data.var () : task Thread_Data.var;
 in
   fun worker_task () = Thread_Data.get worker_task_var;
   fun setmp_worker_task task f x = Thread_Data.setmp worker_task_var (SOME task) f x;
 end;
 
 val worker_group = Option.map Task_Queue.group_of_task o worker_task;
 
 fun the_worker_group () =
   (case worker_group () of
     SOME group => group
   | NONE => raise Fail "Missing worker thread context");
 
 fun worker_subgroup () = new_group (worker_group ());
 
 fun worker_joining e =
   (case worker_task () of
     NONE => e ()
   | SOME task => Task_Queue.joining task e);
 
 fun worker_waiting deps e =
   (case worker_task () of
     NONE => e ()
   | SOME task => Task_Queue.waiting task deps e);
 
 
 (* datatype future *)
 
 type 'a result = 'a Exn.result Single_Assignment.var;
 
 datatype 'a future =
   Value of 'a Exn.result |
   Future of
    {promised: bool,
     task: task,
     result: 'a result};
 
 fun task_of (Value _) = Task_Queue.dummy_task
   | task_of (Future {task, ...}) = task;
 
 fun peek (Value res) = SOME res
   | peek (Future {result, ...}) = Single_Assignment.peek result;
 
 fun is_finished x = is_some (peek x);
 
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
       NONE => PolyML.PrettyString "<future>"
     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 
 
 (** scheduling **)
 
 (* synchronization *)
 
 val scheduler_event = ConditionVar.conditionVar ();
 val work_available = ConditionVar.conditionVar ();
 val work_finished = ConditionVar.conditionVar ();
 
 local
   val lock = Mutex.mutex ();
 in
 
 fun SYNCHRONIZED name = Multithreading.synchronized name lock;
 
 fun wait cond = (*requires SYNCHRONIZED*)
   Multithreading.sync_wait NONE cond lock;
 
 fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
   Multithreading.sync_wait (SOME (Time.now () + timeout)) cond lock;
 
 fun signal cond = (*requires SYNCHRONIZED*)
   ConditionVar.signal cond;
 
 fun broadcast cond = (*requires SYNCHRONIZED*)
   ConditionVar.broadcast cond;
 
 end;
 
 
 (* global state *)
 
 val queue = Unsynchronized.ref Task_Queue.empty;
 val next = Unsynchronized.ref 0;
 val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
 val canceled = Unsynchronized.ref ([]: group list);
 val do_shutdown = Unsynchronized.ref false;
 val max_workers = Unsynchronized.ref 0;
 val max_active = Unsynchronized.ref 0;
 
 val status_ticks = Unsynchronized.ref 0;
 val last_round = Unsynchronized.ref Time.zeroTime;
 val next_round = seconds 0.05;
 
 datatype worker_state = Working | Waiting | Sleeping;
 val workers = Unsynchronized.ref ([]: (Thread.thread * worker_state Unsynchronized.ref) list);
 
 fun count_workers state = (*requires SYNCHRONIZED*)
   fold (fn (_, state_ref) => fn i => if ! state_ref = state then i + 1 else i) (! workers) 0;
 
 
 (* ML statistics *)
 
 fun ML_statistics () = (*requires SYNCHRONIZED*)
   let
     val {ready, pending, running, passive, urgent} = Task_Queue.status (! queue);
     val workers_total = length (! workers);
     val workers_active = count_workers Working;
     val workers_waiting = count_workers Waiting;
   in
     ML_Statistics.set
      {tasks_ready = ready,
       tasks_pending = pending,
       tasks_running = running,
       tasks_passive = passive,
       tasks_urgent = urgent,
       workers_total = workers_total,
       workers_active = workers_active,
       workers_waiting = workers_waiting}
   end;
 
 
 (* cancellation primitives *)
 
 fun cancel_now group = (*requires SYNCHRONIZED*)
   let
     val running = Task_Queue.cancel (! queue) group;
     val _ = running |> List.app (fn thread =>
       if Isabelle_Thread.is_self thread then ()
       else Isabelle_Thread.interrupt_unsynchronized thread);
   in running end;
 
 fun cancel_all () = (*requires SYNCHRONIZED*)
   let
     val (groups, threads) = Task_Queue.cancel_all (! queue);
     val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads;
   in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
  (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
   broadcast scheduler_event);
 
 fun interruptible_task f x =
   Thread_Attributes.with_attributes
     (if is_some (worker_task ())
      then Thread_Attributes.private_interrupts
      else Thread_Attributes.public_interrupts)
     (fn _ => f x)
   before Thread_Attributes.expose_interrupt ();
 
 
 (* worker threads *)
 
 fun worker_exec (task, jobs) =
   let
     val group = Task_Queue.group_of_task task;
     val valid = not (Task_Queue.is_canceled group);
     val ok =
       Task_Queue.running task (fn () =>
         setmp_worker_task task (fn () =>
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     val _ =
       if ! Multithreading.trace >= 2 then
         Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) []
       else ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
         val test = Exn.capture Thread_Attributes.expose_interrupt ();
         val _ =
           if ok andalso not (Exn.is_interrupt_exn test) then ()
           else if null (cancel_now group) then ()
           else cancel_later group;
         val _ = broadcast work_finished;
         val _ = if maximal then () else signal work_available;
       in () end);
   in () end;
 
 fun worker_wait worker_state cond = (*requires SYNCHRONIZED*)
   (case AList.lookup Thread.equal (! workers) (Thread.self ()) of
     SOME state => Unsynchronized.setmp state worker_state wait cond
   | NONE => wait cond);
 
 fun worker_next () = (*requires SYNCHRONIZED*)
   if length (! workers) > ! max_workers then
     (Unsynchronized.change workers (AList.delete Thread.equal (Thread.self ()));
      signal work_available;
      NONE)
   else
     let val urgent_only = count_workers Working > ! max_active in
       (case Unsynchronized.change_result queue (Task_Queue.dequeue (Thread.self ()) urgent_only) of
         NONE => (worker_wait Sleeping work_available; worker_next ())
       | some => (signal work_available; some))
     end;
 
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next ()) of
     NONE => ()
   | SOME work => (worker_exec work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   let
     val worker =
       Isabelle_Thread.fork
         {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
         (fn () => worker_loop name);
   in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
   handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
 
 
 (* scheduler *)
 
 fun scheduler_end () = (*requires SYNCHRONIZED*)
   (ML_statistics (); scheduler := NONE);
 
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
     val now = Time.now ();
     val tick = ! last_round + next_round <= now;
     val _ = if tick then last_round := now else ();
 
 
     (* runtime status *)
 
     val _ =
       if tick then Unsynchronized.change status_ticks (fn i => i + 1) else ();
     val _ =
       if tick andalso ! status_ticks mod (if ! Multithreading.trace >= 1 then 2 else 5) = 0
       then ML_statistics () else ();
 
     val _ =
       if not tick orelse forall (Thread.isActive o #1) (! workers) then ()
       else
         let
           val (alive, dead) = List.partition (Thread.isActive o #1) (! workers);
           val _ = workers := alive;
         in
           Multithreading.tracing 0 (fn () =>
             "SCHEDULER: disposed " ^ string_of_int (length dead) ^ " dead worker threads")
         end;
 
 
     (* worker pool adjustments *)
 
     val max_active0 = ! max_active;
     val max_workers0 = ! max_workers;
 
     val workers_waiting = count_workers Waiting;
 
     val m =
       if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0
       else Multithreading.max_threads ();
     val _ = max_active := m;
     val _ = max_workers :=
       Int.max (2 * m, if workers_waiting > 0 then workers_waiting + 1 else 0);
 
     val missing = ! max_workers - length (! workers);
     val _ =
       if missing > 0 then
         funpow missing (fn () =>
           ignore (worker_start ("worker " ^ string_of_int (Unsynchronized.inc next)))) ()
       else ();
 
     val _ =
       if ! max_active = max_active0 andalso ! max_workers = max_workers0 then ()
       else signal work_available;
 
 
     (* canceled groups *)
 
     val _ =
       if null (! canceled) then ()
       else
        (Multithreading.tracing 1 (fn () =>
           string_of_int (length (! canceled)) ^ " canceled groups");
         Unsynchronized.change canceled (filter_out (null o cancel_now));
         signal work_available);
 
 
     (* delay loop *)
 
     val _ = Exn.release (wait_timeout next_round scheduler_event);
 
 
     (* shutdown *)
 
     val continue = not (! do_shutdown andalso null (! workers));
     val _ = if continue then () else scheduler_end ();
 
     val _ = broadcast scheduler_event;
   in continue end
   handle exn =>
    (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
     if Exn.is_interrupt exn then
      (List.app cancel_later (cancel_all ());
       signal work_available; true)
     else
      (scheduler_end ();
       Exn.reraise exn));
 
 fun scheduler_loop () =
  (while
     Thread_Attributes.with_attributes
       (Thread_Attributes.sync_interrupts Thread_Attributes.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
   do (); last_round := Time.zeroTime);
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
 
 fun scheduler_check () = (*requires SYNCHRONIZED*)
  (do_shutdown := false;
   if scheduler_active () then ()
   else
     scheduler :=
       SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
         scheduler_loop));
 
 
 
 (** futures **)
 
 (* cancel *)
 
 fun cancel_group_unsynchronized group = (*requires SYNCHRONIZED*)
   let
     val _ = if null (cancel_now group) then () else cancel_later group;
     val _ = signal work_available;
     val _ = scheduler_check ();
   in () end;
 
 fun cancel_group group =
   SYNCHRONIZED "cancel_group" (fn () => cancel_group_unsynchronized group);
 
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
 
 
 (* results *)
 
 fun error_message pos ((serial, msg), exec_id) =
   Position.setmp_thread_data pos (fn () =>
-    let val id = Position.get_id pos in
+    let val id = Position.id_of pos in
       if is_none id orelse is_none exec_id orelse id = exec_id
       then Output.error_message' (serial, msg) else ()
     end) ();
 
 fun identify_result pos res =
   res |> Exn.map_exn (fn exn =>
     let val exec_id =
-      (case Position.get_id pos of
+      (case Position.id_of pos of
         NONE => []
       | SOME id => [(Markup.exec_idN, id)])
     in Par_Exn.identify exec_id exn end);
 
 fun assign_result group result res =
   let
     val _ = Single_Assignment.assign result res
       handle exn as Fail _ =>
         (case Single_Assignment.peek result of
           SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
         | _ => Exn.reraise exn);
     val ok =
       (case the (Single_Assignment.peek result) of
         Exn.Exn exn =>
           (SYNCHRONIZED "cancel" (fn () => Task_Queue.cancel_group group exn); false)
       | Exn.Res _ => true);
   in ok end;
 
 
 (* future jobs *)
 
 fun future_job group atts (e: unit -> 'a) =
   let
     val result = Single_Assignment.var "future" : 'a result;
     val pos = Position.thread_data ();
     val context = Context.get_generic_context ();
     fun job ok =
       let
         val res =
           if ok then
             Exn.capture (fn () =>
               Thread_Attributes.with_attributes atts (fn _ =>
                 (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
           else Exn.interrupt_exn;
       in assign_result group result (identify_result pos res) end;
   in (result, job) end;
 
 
 (* fork *)
 
 type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
 val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
 
 fun forks ({name, group, deps, pri, interrupts}: params) es =
   if null es then []
   else
     let
       val grp =
         (case group of
           NONE => worker_subgroup ()
         | SOME grp => grp);
       fun enqueue e queue =
         let
           val atts =
             if interrupts
             then Thread_Attributes.private_interrupts
             else Thread_Attributes.no_interrupts;
           val (result, job) = future_job grp atts e;
           val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
           val future = Future {promised = false, task = task, result = result};
         in (future, queue') end;
     in
       SYNCHRONIZED "enqueue" (fn () =>
         let
           val (futures, queue') = fold_map enqueue es (! queue);
           val _ = queue := queue';
           val minimal = forall (not o Task_Queue.known_task queue') deps;
           val _ = if minimal then signal work_available else ();
           val _ = scheduler_check ();
         in futures end)
     end;
 
 fun fork e =
   (singleton o forks) {name = "fork", group = NONE, deps = [], pri = 0, interrupts = true} e;
 
 
 (* join *)
 
 fun get_result x =
   (case peek x of
     NONE => Exn.Exn (Fail "Unfinished future")
   | SOME res =>
       if Exn.is_interrupt_exn res then
         (case Task_Queue.group_status (Task_Queue.group_of_task (task_of x)) of
           [] => res
         | exns => Exn.Exn (Par_Exn.make exns))
       else res);
 
 local
 
 fun join_next atts deps = (*requires SYNCHRONIZED*)
   if null deps then NONE
   else
     (case Unsynchronized.change_result queue (Task_Queue.dequeue_deps (Thread.self ()) deps) of
       (NONE, []) => NONE
     | (NONE, deps') =>
        (worker_waiting deps' (fn () =>
           Thread_Attributes.with_attributes atts (fn _ =>
             Exn.release (worker_wait Waiting work_finished)));
         join_next atts deps')
     | (SOME work, deps') => SOME (work, deps'));
 
 fun join_loop atts deps =
   (case SYNCHRONIZED "join" (fn () => join_next atts deps) of
     NONE => ()
   | SOME (work, deps') => (worker_joining (fn () => worker_exec work); join_loop atts deps'));
 
 in
 
 fun join_results xs =
   let
     val _ =
       if forall is_finished xs then ()
       else if is_some (worker_task ()) then
         Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
           (fn orig_atts => join_loop orig_atts (map task_of xs))
       else
         xs |> List.app
           (fn Value _ => ()
             | Future {result, ...} => ignore (Single_Assignment.await result));
   in map get_result xs end;
 
 end;
 
 fun join_result x = singleton join_results x;
 fun joins xs = Par_Exn.release_all (join_results xs);
 fun join x = Exn.release (join_result x);
 
 
 (* forked results: nested parallel evaluation *)
 
 fun forked_results {name, deps} es =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val (group, pri) =
         (case worker_task () of
           SOME task =>
             (new_group (SOME (Task_Queue.group_of_task task)), Task_Queue.pri_of_task task)
         | NONE => (new_group NONE, 0));
       val futures =
         forks {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} es;
     in
       restore_attributes join_results futures
         handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
     end) ();
 
 
 (* task context for running thread *)
 
 fun task_context name group f x =
   Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
     let
       val (result, job) = future_job group orig_atts (fn () => f x);
       val task =
         SYNCHRONIZED "enroll" (fn () =>
           Unsynchronized.change_result queue (Task_Queue.enroll (Thread.self ()) name group));
       val _ = worker_exec (task, [job]);
     in
       (case Single_Assignment.peek result of
         NONE => raise Fail "Missing task context result"
       | SOME res => Exn.release res)
     end);
 
 
 (* scheduling parameters *)
 
 fun enabled () =
   let val threads = Multithreading.max_threads () in
     threads > 1 andalso
       let val lim = threads * Options.default_int "parallel_limit"
       in lim <= 0 orelse SYNCHRONIZED "enabled" (fn () => Task_Queue.total_jobs (! queue) < lim) end
   end;
 
 val relevant = (fn [] => false | [_] => false | _ => enabled ());
 
 fun proofs_enabled n =
   ! Multithreading.parallel_proofs >= n andalso is_some (worker_task ()) andalso enabled ();
 
 fun proofs_enabled_timing t =
   proofs_enabled 1 andalso Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
 
 
 (* fast-path operations -- bypass task queue if possible *)
 
 fun value_result (res: 'a Exn.result) =
   let
     val task = Task_Queue.dummy_task;
     val group = Task_Queue.group_of_task task;
     val result = Single_Assignment.var "value" : 'a result;
     val _ = assign_result group result (identify_result (Position.thread_data ()) res);
   in Future {promised = false, task = task, result = result} end;
 
 fun value x = value_result (Exn.Res x);
 
 fun cond_forks args es =
   if enabled () then forks args es
   else map (fn e => value_result (Exn.interruptible_capture e ())) es;
 
 fun map_future f x =
   if is_finished x then value_result (Exn.interruptible_capture (f o join) x)
   else
     let
       val task = task_of x;
       val group = Task_Queue.group_of_task task;
       val (result, job) =
         future_job group Thread_Attributes.private_interrupts (fn () => f (join x));
 
       val extended = SYNCHRONIZED "extend" (fn () =>
         (case Task_Queue.extend task job (! queue) of
           SOME queue' => (queue := queue'; true)
         | NONE => false));
     in
       if extended then Future {promised = false, task = task, result = result}
       else
         (singleton o cond_forks)
           {name = "map_future", group = SOME group, deps = [task],
             pri = Task_Queue.pri_of_task task, interrupts = true}
           (fn () => f (join x))
     end;
 
 
 (* promised futures -- fulfilled by external means *)
 
 fun promise_name name abort : 'a future =
   let
     val group = worker_subgroup ();
     val result = Single_Assignment.var "promise" : 'a result;
     fun assign () = assign_result group result Exn.interrupt_exn
       handle Fail _ => true
         | exn =>
             if Exn.is_interrupt exn
             then raise Fail "Concurrent attempt to fulfill promise"
             else Exn.reraise exn;
     fun job () =
       Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
         (fn _ => Exn.release (Exn.capture assign () before abort ()));
     val task = SYNCHRONIZED "enqueue_passive" (fn () =>
       Unsynchronized.change_result queue (Task_Queue.enqueue_passive group name job));
   in Future {promised = true, task = task, result = result} end;
 
 fun promise abort = promise_name "passive" abort;
 
 fun fulfill_result (Future {promised = true, task, result}) res =
       let
         val group = Task_Queue.group_of_task task;
         val pos = Position.thread_data ();
         fun job ok =
           assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
         val _ =
           Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
             let
               val passive_job =
                 SYNCHRONIZED "fulfill_result" (fn () =>
                   Unsynchronized.change_result queue
                     (Task_Queue.dequeue_passive (Thread.self ()) task));
             in
               (case passive_job of
                 SOME true => worker_exec (task, [job])
               | SOME false => ()
               | NONE => ignore (job (not (Task_Queue.is_canceled group))))
             end);
         val _ =
           if is_some (Single_Assignment.peek result) then ()
           else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
       in () end
   | fulfill_result _ _ = raise Fail "Not a promised future";
 
 fun fulfill x res = fulfill_result x (Exn.Res res);
 
 
 (* snapshot: current tasks of groups *)
 
 fun snapshot [] = []
   | snapshot groups =
       SYNCHRONIZED "snapshot" (fn () =>
         Task_Queue.group_tasks (! queue) groups);
 
 
 (* shutdown *)
 
 fun shutdown () =
   if is_some (worker_task ()) then
     raise Fail "Cannot shutdown while running as worker thread"
   else
     SYNCHRONIZED "shutdown" (fn () =>
       while scheduler_active () do
        (do_shutdown := true;
         Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
         wait_timeout next_round scheduler_event));
 
 
 (*final declarations of this structure!*)
 val map = map_future;
 
 end;
 
 type 'a future = 'a Future.future;
diff --git a/src/Pure/General/position.ML b/src/Pure/General/position.ML
--- a/src/Pure/General/position.ML
+++ b/src/Pure/General/position.ML
@@ -1,295 +1,296 @@
 (*  Title:      Pure/General/position.ML
     Author:     Makarius
 
 Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
 symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
 right-open interval offset .. end_offset (exclusive).
 *)
 
 signature POSITION =
 sig
   eqtype T
   val ord: T ord
   val make: Thread_Position.T -> T
   val dest: T -> Thread_Position.T
   val line_of: T -> int option
   val offset_of: T -> int option
   val end_offset_of: T -> int option
   val file_of: T -> string option
+  val id_of: T -> string option
   val advance: Symbol.symbol -> T -> T
   val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
   val none: T
   val start: T
   val file_name: string -> Properties.T
   val file_only: string -> T
   val file: string -> T
   val line_file_only: int -> string -> T
   val line_file: int -> string -> T
   val line: int -> T
   val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
-  val get_id: T -> string option
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
   val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val entity_properties_of: bool -> serial -> T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
   type report = T * Markup.T
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
   val store_reports: report_text list Unsynchronized.ref ->
     T list -> ('a -> Markup.T list) -> 'a -> unit
   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here_strs: T -> string * string
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
   val no_range: range
   val no_range_position: T -> T
   val range_position: range -> T
   val range: T * T -> range
   val range_of_properties: Properties.T -> range
   val properties_of_range: range -> Properties.T
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
   val default: T -> bool * T
 end;
 
 structure Position: POSITION =
 struct
 
 (* datatype position *)
 
 datatype T = Pos of (int * int * int) * Properties.T;
 
 fun dest2 f = apply2 (fn Pos p => f p);
 
 val ord =
   pointer_eq_ord
    (int_ord o dest2 (#1 o #1) |||
     int_ord o dest2 (#2 o #1) |||
     int_ord o dest2 (#3 o #1) |||
     Properties.ord o dest2 #2);
 
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
     [Markup.fileN, Markup.idN];
 
 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
 
 fun valid (i: int) = i > 0;
+fun maybe_valid i = if valid i then SOME i else NONE;
 fun if_valid i i' = if valid i then i' else i;
 
 
 (* fields *)
 
-fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
-fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
-fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
+fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
+fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
+fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
 
 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
+fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
 
 
 (* advance *)
 
 fun advance_count "\n" (i: int, j: int, k: int) =
       (if_valid i (i + 1), if_valid j (j + 1), k)
   | advance_count s (i, j, k) =
       if Symbol.not_eof s then (i, if_valid j (j + 1), k)
       else (i, j, k);
 
 fun invalid_count (i, j, _: int) =
   not (valid i orelse valid j);
 
 fun advance sym (pos as (Pos (count, props))) =
   if invalid_count count then pos else Pos (advance_count sym count, props);
 
 fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
   if offset = 0 orelse invalid_count count then pos
   else if offset < 0 then raise Fail "Illegal offset"
   else if valid i then raise Fail "Illegal line position"
   else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
 
 
 (* distance of adjacent positions *)
 
 fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
   if valid j andalso valid j' then SOME (j' - j) else NONE;
 
 
 (* make position *)
 
 val none = Pos ((0, 0, 0), []);
 val start = Pos ((1, 1, 0), []);
 
 
 fun file_name "" = []
   | file_name name = [(Markup.fileN, name)];
 
 fun file_only name = Pos ((0, 0, 0), file_name name);
 fun file name = Pos ((1, 1, 0), file_name name);
 
 fun line_file_only i name = Pos ((i, 0, 0), file_name name);
 fun line_file i name = Pos ((i, 1, 0), file_name name);
 fun line i = line_file i "";
 
 fun get_props (Pos (_, props)) = props;
 
 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
-fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
-fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id);
+fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
-fun parse_id pos = Option.map Value.parse_int (get_id pos);
+fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
 fun id_properties_of pos =
-  (case get_id pos of
+  (case id_of pos of
     SOME id => [(Markup.idN, id)]
   | NONE => []);
 
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   if is_none (file_of pos) then
     (case parse_id pos of
       SOME id =>
         (case adjust id of
           SOME offset =>
             let val Pos (count, _) = advance_offsets offset pos
             in Pos (count, Properties.remove Markup.idN props) end
         | NONE => pos)
     | NONE => pos)
   else pos;
 
 
 (* markup properties *)
 
 fun get props name =
   (case Properties.get props name of
     NONE => 0
   | SOME s => Value.parse_int s);
 
 fun of_properties props =
   make {line = get props Markup.lineN,
     offset = get props Markup.offsetN,
     end_offset = get props Markup.end_offsetN,
     props = props};
 
 fun value k i = if valid i then [(k, Value.print_int i)] else [];
 
 fun properties_of (Pos ((i, j, k), props)) =
   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
 
 fun offset_properties_of (Pos ((_, j, k), _)) =
   value Markup.offsetN j @ value Markup.end_offsetN k;
 
 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
 
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
 
 fun entity_properties_of def serial pos =
   if def then (Markup.defN, Value.print_int serial) :: properties_of pos
   else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
 
 val markup = Markup.properties o properties_of;
 
 
 (* reports *)
 
-fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
 fun report_text pos markup txt = Output.report [reported_text pos markup txt];
 fun report pos markup = report_text pos markup "";
 
 type report = T * Markup.T;
 type report_text = report * string;
 
 val reports_text =
   map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
   #> Output.report;
 
 val reports = map (rpair "") #> reports_text;
 
 fun store_reports _ [] _ _ = ()
   | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
 
 fun append_reports (r: report_text list Unsynchronized.ref) reports =
   Unsynchronized.change r (append (map (rpair "") reports));
 
 
 (* here: user output *)
 
 fun here_strs pos =
   (case (line_of pos, file_of pos) of
     (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
   | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
   | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
 
 fun here pos =
   let
     val props = properties_of pos;
     val (s1, s2) = here_strs pos;
   in
     if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
 val here_list = map here #> distinct (op =) #> implode;
 
 
 (* range *)
 
 type range = T * T;
 
 val no_range = (none, none);
 
 fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
 fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
 fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
 
 fun range_of_properties props =
   let
     val pos = of_properties props;
     val pos' =
       make {line = get props Markup.end_lineN,
         offset = get props Markup.end_offsetN,
         end_offset = 0,
         props = props};
   in (pos, pos') end;
 
 fun properties_of_range (pos, pos') =
   properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
 
 
 (* thread data *)
 
 val thread_data = make o Thread_Position.get;
 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
 fun default pos =
   if pos = none then (false, thread_data ())
   else (true, pos);
 
 end;
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,507 +1,507 @@
 (*  Title:      Pure/PIDE/command.ML
     Author:     Makarius
 
 Prover command execution: read -- eval -- print.
 *)
 
 signature COMMAND =
 sig
   type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}
   val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file
   val read_thy: Toplevel.state -> theory
   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
     blob Exn.result list * int -> Token.T list -> Toplevel.transition
   val read_span: Keyword.keywords -> Toplevel.state -> Path.T -> (unit -> theory) ->
     Command_Span.span -> Toplevel.transition
   type eval
   val eval_command_id: eval -> Document_ID.command
   val eval_exec_id: eval -> Document_ID.exec
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_command: eval -> Toplevel.transition
   val eval_result_state: eval -> Toplevel.state
   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     blob Exn.result list * int -> Document_ID.command -> Token.T list -> eval -> eval
   type print
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   val print0: {pri: int, print_fn: print_fn} -> eval -> print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
   val parallel_print: print -> bool
   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 init_exec: theory option -> exec
   val no_exec: exec
   val exec_ids: exec option -> Document_ID.exec list
   val exec: Document_ID.execution -> exec -> unit
   val exec_parallel_prints: Document_ID.execution -> Future.task list -> exec -> exec option
 end;
 
 structure Command: COMMAND =
 struct
 
 (** main phases of execution **)
 
 fun task_context group f =
   f
   |> Future.interruptible_task
   |> Future.task_context "Command.run_process" group;
 
 
 (* read *)
 
 type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option};
 
 fun read_file_node file_node master_dir pos delimited src_path =
   let
     val _ =
       if Context_Position.pide_reports ()
       then Position.report pos (Markup.language_path delimited) else ();
 
     fun read_file () =
       let
         val path = File.check_file (File.full_path master_dir src_path);
         val text = File.read path;
         val file_pos = Path.position path;
       in (text, file_pos) end;
 
     fun read_url () =
       let
         val text = Isabelle_System.download file_node;
         val file_pos = Position.file file_node;
       in (text, file_pos) end;
 
     val (text, file_pos) =
       (case try Url.explode file_node of
         NONE => read_file ()
       | SOME (Url.File _) => read_file ()
       | _ => read_url ());
 
     val lines = split_lines text;
     val digest = SHA1.digest text;
   in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end
   handle ERROR msg => error (msg ^ Position.here pos);
 
 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
+      (case Position.id_of (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 master_dir (blobs, blobs_index) toks =
   (case Outer_Syntax.parse_spans toks of
     [Command_Span.Span (Command_Span.Command_Span _, _)] =>
       (case try (nth toks) blobs_index of
         SOME tok =>
           let
             val source = Token.input_of tok;
             val pos = Input.pos_of source;
             val delimited = Input.is_delimited source;
 
             fun make_file (Exn.Res {file_node, src_path, content = NONE}) =
                   Exn.interruptible_capture (fn () =>
                     read_file_node file_node master_dir pos delimited src_path) ()
               | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) =
                   (Position.report pos (Markup.language_path delimited);
                     Exn.Res (blob_file src_path lines digest file_node))
               | make_file (Exn.Exn e) = Exn.Exn e;
             val files = map make_file blobs;
           in
             toks |> map_index (fn (i, tok) =>
               if i = blobs_index then Token.put_files files tok else tok)
           end
       | NONE => toks)
   | _ => toks);
 
 fun reports_of_token keywords tok =
   let
     val malformed_symbols =
       Input.source_explode (Token.input_of tok)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
 
 fun read_thy st = Toplevel.theory_of st
   handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy;
 
 fun read keywords thy master_dir init blobs_info span =
   let
     val command_reports = Outer_Syntax.command_reports thy;
     val token_reports = map (reports_of_token keywords) span;
     val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
 
     val verbatim =
       span |> map_filter (fn tok =>
         if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE);
     val _ =
       if null verbatim then ()
       else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^
         Position.here_list verbatim);
   in
     if exists #1 token_reports
     then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax"
     else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span)
   end;
 
 end;
 
 fun read_span keywords st master_dir init =
   Command_Span.content #> read keywords (read_thy st) master_dir init ([], ~1);
 
 
 (* eval *)
 
 type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
 
 fun init_eval_state opt_thy =
  {failed = false,
   command = Toplevel.empty,
   state =
     (case opt_thy of
       NONE => Toplevel.init_toplevel ()
     | SOME thy => Toplevel.theory_toplevel thy)};
 
 datatype eval =
   Eval of
     {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy};
 
 fun eval_command_id (Eval {command_id, ...}) = command_id;
 
 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 {eval_process, ...}) =
   Exn.release (Lazy.finished_result eval_process);
 
 val eval_result_command = #command o eval_result;
 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 if Keyword.is_theory_end keywords name then
         (case Toplevel.reset_notepad st0 of
           NONE => Toplevel.reset_theory st0
         | some => some)
       else NONE;
   in
     (case res of
       NONE => st0
     | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st))
   end) ();
 
 fun run keywords int tr st =
   if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     let
       val (tr1, tr2) = Toplevel.fork_presentation tr;
       val _ =
         Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
           (fn () => Toplevel.command_exception int tr1 st);
     in Toplevel.command_errors int tr2 st end
   else Toplevel.command_errors int tr st;
 
 fun check_token_comments ctxt tok =
   (Document_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); [])
     handle exn =>
       if Exn.is_interrupt exn then Exn.reraise exn
       else Runtime.exn_messages exn;
 
 fun check_span_comments ctxt span tr =
   Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) ();
 
 fun report_indent tr st =
   (case try Toplevel.proof_of st of
     SOME prf =>
       let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in
         if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then
           (case try (Thm.nprems_of o #goal o Proof.goal) prf of
             NONE => ()
           | SOME 0 => ()
           | SOME n =>
               let val report = Markup.markup_only (Markup.command_indent (n - 1));
               in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end)
         else ()
       end
   | NONE => ());
 
 fun status tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
 
 fun eval_state keywords span tr ({state, ...}: eval_state) =
   let
     val _ = Thread_Attributes.expose_interrupt ();
 
     val st = reset_state keywords tr state;
 
     val _ = report_indent tr st;
     val _ = status tr Markup.running;
     val (errs1, result) = run keywords true tr st;
     val errs2 =
       (case result of
         NONE => []
       | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr);
     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 (status tr Markup.canceled; Exn.interrupt ()) else ();
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
         let
           val _ =
             if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso
               can (Toplevel.end_theory Position.none) st'
             then status tr Markup.finalized else ();
           val _ = status tr Markup.finished;
         in {failed = false, command = tr, state = st'} end)
   end;
 
 in
 
 fun eval keywords master_dir init blobs_info command_id 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_info span |> Toplevel.exec_id exec_id) ();
       in eval_state keywords span tr eval_state0 end;
   in
     Eval {command_id = command_id, exec_id = exec_id,
       eval_process = Lazy.lazy_name "Command.eval" 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 Exn.reraise exn
       else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages 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);
 
 fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval =
   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_name "Command.print" process}
   end;
 
 fun bad_print name_args exn =
   make_print name_args {delay = NONE, pri = 0, persistent = false,
     strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
 
 in
 
 fun print0 {pri, print_fn} =
   make_print ("", [serial_string ()])
     {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
 
 fun print command_visible command_overlays keywords command_name eval old_prints =
   let
     val print_functions = Synchronized.value print_functions;
 
     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 eval)
         | Exn.Exn exn => SOME (bad_print (name, args) exn eval))
       end;
 
     fun get_print (name, args) =
       (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of
         NONE =>
           (case AList.lookup (op =) print_functions name of
             NONE =>
               SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval)
           | SOME get_pr => new_print (name, args) get_pr)
       | some => some);
 
     val retained_prints =
       filter (fn print => print_finished print andalso print_persistent print) old_prints;
     val visible_prints =
       if command_visible then
         fold (fn (name, _) => cons (name, [])) print_functions command_overlays
         |> sort_distinct overlay_ord
         |> map_filter get_print
       else [];
     val new_prints = visible_prints @ retained_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   end;
 
 fun parallel_print (Print {pri, ...}) =
   pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print");
 
 fun print_function name f =
   Synchronized.change print_functions (fn funs =>
    (if name = "" then error "Unnamed print function" else ();
     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 = Task_Queue.urgent_pri + 2, 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 Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
       then
         SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
           print_fn = fn _ => fn st =>
             if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
             else ()}
       else NONE);
 
 
 (* combined execution *)
 
 type exec = eval * print list;
 
 fun init_exec opt_thy : exec =
   (Eval
     {command_id = Document_ID.none, exec_id = Document_ID.none,
       eval_process = Lazy.value (init_eval_state opt_thy)}, []);
 
 val no_exec = init_exec NONE;
 
 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 (task_context group (fn () => Lazy.force_result {strict = true} 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 fork_print execution_id deps (Print {name, delay, pri, exec_id, print_process, ...}) =
   let
     val group = Future.worker_subgroup ();
     fun fork () =
       ignore ((singleton o Future.forks)
         {name = name, group = SOME group, deps = 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 {physical = true} (Time.now () + d) fork))
   end;
 
 fun run_print execution_id (print as Print {exec_id, print_process, ...}) =
   if ignore_process print_process then ()
   else if parallel_print print then fork_print execution_id [] print
   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);
 
 fun exec_parallel_prints execution_id deps (exec as (Eval {eval_process, ...}, prints)) =
   if Lazy.is_finished eval_process
   then (List.app (fork_print execution_id deps) prints; NONE)
   else SOME exec;
 
 end;
 
 end;
diff --git a/src/Pure/PIDE/document.ML b/src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML
+++ b/src/Pure/PIDE/document.ML
@@ -1,921 +1,921 @@
 (*  Title:      Pure/PIDE/document.ML
     Author:     Makarius
 
 Document as collection of named nodes, each consisting of an editable
 list of commands, associated with asynchronous execution process.
 *)
 
 signature DOCUMENT =
 sig
   val timing: bool Unsynchronized.ref
   type node_header = {master: string, header: Thy_Header.header, errors: string list}
   type overlay = Document_ID.command * (string * string list)
   datatype node_edit =
     Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
     Perspective of bool * Document_ID.command list * overlay list
   type edit = string * node_edit
   type state
   val init_state: state
   val define_blob: string -> string -> state -> state
   type blob_digest = {file_node: string, src_path: Path.T, digest: string option} Exn.result
   type command =
    {command_id: Document_ID.command,
     name: string,
     parents: string list,
     blobs_digests: blob_digest list,
     blobs_index: int,
     tokens: ((int * int) * string) list}
   val define_command: command -> state -> state
   val command_exec: state -> string -> Document_ID.command -> Command.exec option
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
     string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
 
 structure Document: DOCUMENT =
 struct
 
 val timing = Unsynchronized.ref false;
 fun timeit msg e = cond_timeit (! timing) msg e;
 
 
 
 (** document structure **)
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
 
 type node_header =
   {master: string, header: Thy_Header.header, errors: string list};
 
 type perspective =
  {required: bool,  (*required node*)
   visible: Inttab.set,  (*visible commands*)
   visible_last: Document_ID.command option,  (*last visible command*)
   overlays: (string * string list) list Inttab.table};  (*command id -> print functions with args*)
 
 structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
   keywords: Keyword.keywords option,  (*outer syntax keywords*)
   perspective: perspective,  (*command perspective*)
   entries: Command.exec option Entries.T,  (*command entries with executions*)
   result: (Document_ID.command * Command.eval) option,  (*result of last execution*)
   consolidated: unit lazy}  (*consolidated status of eval forks*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with
 
 fun make_node (header, keywords, perspective, entries, result, consolidated) =
   Node {header = header, keywords = keywords, perspective = perspective,
     entries = entries, result = result, consolidated = consolidated};
 
 fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
   make_node (f (header, keywords, perspective, entries, result, consolidated));
 
 fun make_perspective (required, command_ids, overlays) : perspective =
  {required = required,
   visible = Inttab.make_set command_ids,
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
 val no_header: node_header =
   {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node =
   make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
 
 fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
   Inttab.is_empty visible andalso
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
 fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
   header = no_header andalso
   is_none keywords andalso
   is_no_perspective perspective andalso
   Entries.is_empty entries andalso
   is_none result andalso
   Lazy.is_finished consolidated;
 
 
 (* basic components *)
 
 fun master_directory (Node {header = {master, ...}, ...}) =
   (case try Url.explode master of
     SOME (Url.File path) => path
   | _ => Path.current);
 
 fun set_header master header errors =
   map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
     ({master = master, header = header, errors = errors},
       keywords, perspective, entries, result, consolidated));
 
 fun get_header (Node {header, ...}) = header;
 
 fun set_keywords keywords =
   map_node (fn (header, _, perspective, entries, result, consolidated) =>
     (header, keywords, perspective, entries, result, consolidated));
 
 fun get_keywords (Node {keywords, ...}) = keywords;
 
 fun read_header node span =
   let
     val {header, errors, ...} = get_header node;
     val _ =
       if null errors then ()
       else
         cat_lines errors |>
-        (case Position.get_id (Position.thread_data ()) of
+        (case Position.id_of (Position.thread_data ()) of
           NONE => I
         | SOME id => Protocol_Message.command_positions_yxml id)
         |> error;
     val {name = (name, _), imports, ...} = header;
     val {name = (_, pos), imports = imports', keywords} =
       Thy_Header.read_tokens Position.none span;
     val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports;
   in Thy_Header.make (name, pos) imports'' keywords end;
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 
 fun set_perspective args =
   map_node (fn (header, keywords, _, entries, result, consolidated) =>
     (header, keywords, make_perspective args, entries, result, consolidated));
 
 val required_node = #required o get_perspective;
 val visible_command = Inttab.defined o #visible o get_perspective;
 val visible_last = #visible_last o get_perspective;
 val visible_node = is_some o visible_last
 val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
   map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
     (header, keywords, perspective, f entries, result, consolidated));
 
 fun get_entries (Node {entries, ...}) = entries;
 
 fun iterate_entries f = Entries.iterate NONE f o get_entries;
 fun iterate_entries_after start f (Node {entries, ...}) =
   (case Entries.get_after entries start of
     NONE => I
   | SOME id => Entries.iterate (SOME id) f entries);
 
 fun get_result (Node {result, ...}) = result;
 
 fun set_result result =
   map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
     (header, keywords, perspective, entries, result, consolidated));
 
 fun pending_result node =
   (case get_result node of
     SOME (_, eval) => not (Command.eval_finished eval)
   | NONE => false);
 
 fun finished_result node =
   (case get_result node of
     SOME (_, eval) => Command.eval_finished eval
   | NONE => false);
 
 fun finished_result_theory node =
   if finished_result node then
     let
       val (result_id, eval) = the (get_result node);
       val st = Command.eval_result_state eval;
     in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
   else NONE;
 
 val reset_consolidated =
   map_node (fn (header, keywords, perspective, entries, result, _) =>
     (header, keywords, perspective, entries, result, Lazy.lazy I));
 
 fun commit_consolidated (Node {consolidated, ...}) =
   (Lazy.force consolidated; Output.status [Markup.markup_only Markup.consolidated]);
 
 fun consolidated_node (Node {consolidated, ...}) = Lazy.is_finished consolidated;
 
 fun could_consolidate node =
   not (consolidated_node node) andalso is_some (finished_result_theory node);
 
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
 fun update_node name f = default_node name #> String_Graph.map_node name f;
 
 
 (* node edits and associated executions *)
 
 type overlay = Document_ID.command * (string * string list);
 
 datatype node_edit =
   Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
   Perspective of bool * Document_ID.command list * overlay list;
 
 type edit = string * node_edit;
 
 val after_entry = Entries.get_after o get_entries;
 
 fun lookup_entry node id =
   (case Entries.lookup (get_entries node) id of
     NONE => NONE
   | SOME (exec, _) => exec);
 
 fun the_entry node id =
   (case Entries.lookup (get_entries node) id of
     NONE => err_undef "command entry" id
   | SOME (exec, _) => exec);
 
 fun assign_entry (command_id, exec) node =
   if is_none (Entries.lookup (get_entries node) command_id) then node
   else map_entries (Entries.update (command_id, exec)) node;
 
 fun reset_after id entries =
   (case Entries.get_after entries id of
     NONE => entries
   | SOME next => Entries.update (next, NONE) entries);
 
 val edit_node = map_entries o fold
   (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
     | (id, NONE) => Entries.delete_after id #> reset_after id);
 
 
 (* version operations *)
 
 val empty_version = Version String_Graph.empty;
 
 fun nodes_of (Version nodes) = nodes;
 val node_of = get_node o nodes_of;
 
 fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
 
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
     (case node_edit of
       Edits edits => update_node name (edit_node edits) nodes
     | Deps {master, header, errors} =>
         let
           val imports = map fst (#imports header);
           val nodes1 = nodes
             |> default_node name
             |> fold default_node imports;
           val nodes2 = nodes1
             |> String_Graph.Keys.fold
                 (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
           val (nodes3, errors1) =
             (String_Graph.add_deps_acyclic (name, imports) nodes2, errors)
               handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs);
         in String_Graph.map_node name (set_header master header errors1) nodes3 end
     | Perspective perspective => update_node name (set_perspective perspective) nodes);
 
 fun update_keywords name nodes =
   nodes |> String_Graph.map_node name (fn node =>
     if is_empty_node node then node
     else
       let
         val {master, header, errors} = get_header node;
         val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header);
         val keywords =
           Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords);
         val (keywords', errors') =
           (Keyword.add_keywords (#keywords header) keywords, errors)
             handle ERROR msg =>
               (keywords, if member (op =) errors msg then errors else errors @ [msg]);
       in
         node
         |> set_header master header errors'
         |> set_keywords (SOME keywords')
       end);
 
 fun edit_keywords edits (Version nodes) =
   Version
     (fold update_keywords
       (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
       nodes);
 
 fun suppressed_node (nodes: node String_Graph.T) (name, node) =
   String_Graph.is_maximal nodes name andalso is_empty_node node;
 
 fun put_node (name, node) (Version nodes) =
   let
     val nodes1 = update_node name (K node) nodes;
     val nodes2 =
       if suppressed_node nodes1 (name, node)
       then String_Graph.del_node name nodes1
       else nodes1;
   in Version nodes2 end;
 
 end;
 
 
 
 (** main state -- document structure and execution process **)
 
 type blob_digest = {file_node: string, src_path: Path.T, digest: string option} Exn.result;
 
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
   execution_id: Document_ID.execution,  (*dynamic execution id*)
   delay_request: unit future,  (*pending event timer request*)
   parallel_prints: Command.exec list};  (*parallel prints for early execution*)
 
 val no_execution: execution =
   {version_id = Document_ID.none,
    execution_id = Document_ID.none,
    delay_request = Future.value (),
    parallel_prints = []};
 
 fun new_execution version_id delay_request parallel_prints : execution =
   {version_id = version_id,
    execution_id = Execution.start (),
    delay_request = delay_request,
    parallel_prints = parallel_prints};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
   blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
   commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table,
     (*command id -> name, inlined files, token index of files, command span*)
   execution: execution}  (*current execution process*)
 with
 
 fun make_state (versions, blobs, commands, execution) =
   State {versions = versions, blobs = blobs, commands = commands, execution = execution};
 
 fun map_state f (State {versions, blobs, commands, execution}) =
   make_state (f (versions, blobs, commands, execution));
 
 val init_state =
   make_state (Inttab.make [(Document_ID.none, empty_version)],
     Symtab.empty, Inttab.empty, no_execution);
 
 
 (* document versions *)
 
 fun parallel_prints_node node =
   iterate_entries (fn (_, opt_exec) => fn rev_result =>
     (case opt_exec of
       SOME (eval, prints) =>
         (case filter Command.parallel_print prints of
           [] => SOME rev_result
         | prints' => SOME ((eval, prints') :: rev_result))
     | NONE => NONE)) node [] |> rev;
 
 fun define_version version_id version assigned_nodes =
   map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
     let
       val version' = fold put_node assigned_nodes version;
       val versions' = Inttab.update_new (version_id, version') versions
         handle Inttab.DUP dup => err_dup "document version" dup;
       val parallel_prints = maps (parallel_prints_node o #2) assigned_nodes;
       val execution' = new_execution version_id delay_request parallel_prints;
     in (versions', blobs, commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =
   (case Inttab.lookup versions version_id of
     NONE => err_undef "document version" version_id
   | SOME version => version);
 
 fun delete_version version_id versions =
   Inttab.delete version_id versions
     handle Inttab.UNDEF _ => err_undef "document version" version_id;
 
 
 (* inlined files *)
 
 fun define_blob digest text =
   map_state (fn (versions, blobs, commands, execution) =>
     let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs
     in (versions, blobs', commands, execution) end);
 
 fun the_blob (State {blobs, ...}) digest =
   (case Symtab.lookup blobs digest of
     NONE => error ("Undefined blob: " ^ digest)
   | SOME content => content);
 
 fun resolve_blob state (blob_digest: blob_digest) =
   blob_digest |> Exn.map_res (fn {file_node, src_path, digest} =>
     {file_node = file_node, src_path = src_path, content = Option.map (the_blob state) digest});
 
 fun blob_reports pos (blob_digest: blob_digest) =
   (case blob_digest of Exn.Res {file_node, ...} => [(pos, Markup.path file_node)] | _ => []);
 
 
 (* commands *)
 
 type command =
   {command_id: Document_ID.command,
    name: string,
    parents: string list,
    blobs_digests: blob_digest list,
    blobs_index: int,
    tokens: ((int * int) * string) list};
 
 fun define_command {command_id, name, parents, blobs_digests, blobs_index, tokens} =
   map_state (fn (versions, blobs, commands, execution) =>
     let
       val id = Document_ID.print command_id;
       val span =
         Lazy.lazy_name "Document.define_command" (fn () =>
           Position.setmp_thread_data (Position.id_only id)
             (fn () =>
               let
                 val (tokens, _) = fold_map Token.make tokens (Position.id id);
                 val imports =
                   if name = Thy_Header.theoryN then
                     (#imports (Thy_Header.read_tokens Position.none tokens)
                       handle ERROR _ => [])
                   else [];
                 val _ =
                   if length parents = length imports then
                     (parents, imports) |> ListPair.app (fn (parent, (_, pos)) =>
                       let val markup =
                         (case Thy_Info.lookup_theory parent of
                           SOME thy => Theory.get_markup thy
                         | NONE =>
                             (case try Url.explode parent of
                               NONE => Markup.path parent
                             | SOME (Url.File path) => Markup.path (Path.implode path)
                             | SOME _ => Markup.path parent))
                       in Position.report pos markup end)
                   else ();
                 val _ =
                   if blobs_index < 0
                   then (*inlined errors*)
                     map_filter Exn.get_exn blobs_digests
                     |> List.app (Output.error_message o Runtime.exn_message)
                   else (*auxiliary files*)
                     let val pos = Token.pos_of (nth tokens blobs_index)
                     in Position.reports (maps (blob_reports pos) blobs_digests) end;
               in tokens end) ());
       val commands' =
         Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
     in (versions, blobs, commands', execution) end);
 
 fun the_command (State {commands, ...}) command_id =
   (case Inttab.lookup commands command_id of
     NONE => err_undef "command" command_id
   | SOME command => command);
 
 val the_command_name = #1 oo the_command;
 
 
 (* execution *)
 
 fun get_execution (State {execution, ...}) = execution;
 fun get_execution_version state = the_version state (#version_id (get_execution state));
 
 fun command_exec state node_name command_id =
   let
     val version = get_execution_version state;
     val node = get_node (nodes_of version) node_name;
   in the_entry node command_id end;
 
 end;
 
 
 (* remove_versions *)
 
 fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) =>
   let
     val _ =
       member (op =) version_ids (#version_id execution) andalso
         error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution));
 
     val versions' = fold delete_version version_ids versions;
     val commands' =
       (versions', Inttab.empty) |->
         Inttab.fold (fn (_, version) => nodes_of version |>
           String_Graph.fold (fn (_, (node, _)) => node |>
             iterate_entries (fn ((_, command_id), _) =>
               SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
     val blobs' =
       (commands', Symtab.empty) |->
         Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
           fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I));
 
   in (versions', blobs', commands', execution) end);
 
 
 (* document execution *)
 
 fun make_required nodes =
   let
     fun all_preds P =
       String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes []
       |> String_Graph.all_preds nodes
       |> Symtab.make_set;
 
     val all_visible = all_preds visible_node;
     val all_required = all_preds required_node;
   in
     Symtab.fold (fn (a, ()) =>
       exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
         Symtab.update (a, ())) all_visible all_required
   end;
 
 fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
       val {version_id, execution_id, delay_request, parallel_prints} = execution;
 
       val delay = seconds (Options.default_real "editor_execution_delay");
 
       val _ = Future.cancel delay_request;
       val delay_request' = Event_Timer.future {physical = true} (Time.now () + delay);
       val delay = Future.task_of delay_request';
 
       val parallel_prints' = parallel_prints
         |> map_filter (Command.exec_parallel_prints execution_id [delay]);
 
       fun finished_import (name, (node, _)) =
         finished_result node orelse is_some (Thy_Info.lookup_theory name);
 
       val nodes = nodes_of (the_version state version_id);
       val required = make_required nodes;
       val _ =
         nodes |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if Symtab.defined required name orelse visible_node node orelse pending_result node then
               let
                 val future =
                   (singleton o Future.forks)
                    {name = "theory:" ^ name,
                     group = SOME (Future.new_group NONE),
                     deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps,
                     pri = 0, interrupts = false}
                   (fn () =>
                    (Execution.worker_task_active true name;
                     if forall finished_import deps then
                       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 ()
                     else ();
                     Execution.worker_task_active false name)
                       handle exn =>
                        (Output.system_message (Runtime.exn_message exn);
                         Execution.worker_task_active false name;
                         Exn.reraise exn));
               in (node, SOME (Future.task_of future)) end
             else (node, NONE));
       val execution' =
         {version_id = version_id, execution_id = execution_id,
           delay_request = delay_request', parallel_prints = parallel_prints'};
     in (versions, blobs, commands, execution') end));
 
 
 
 (** document update **)
 
 (* exec state assignment *)
 
 type assign_update = Command.exec option Inttab.table;  (*command id -> exec*)
 
 val assign_update_empty: assign_update = Inttab.empty;
 fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
 fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab;
 fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
 
 fun assign_update_new upd (tab: assign_update) =
   Inttab.update_new upd tab
     handle Inttab.DUP dup => err_dup "exec state assignment" dup;
 
 fun assign_update_result (tab: assign_update) =
   Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab [];
 
 
 (* update *)
 
 local
 
 fun init_theory deps node span =
   let
     val master_dir = master_directory node;
     val header = read_header node span;
     val imports = #imports header;
 
     fun maybe_eval_result eval = Command.eval_result_state eval
       handle Fail _ => Toplevel.init_toplevel ();
 
     fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
       handle ERROR msg => (Output.error_message msg; NONE);
 
     val parents_reports =
       imports |> map_filter (fn (import, pos) =>
         (case Thy_Info.lookup_theory import of
           NONE =>
             maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
                 NONE => Toplevel.init_toplevel ()
               | SOME (_, eval) => maybe_eval_result eval)
             |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))
         | SOME thy => SOME (thy, (Position.none, Markup.empty))));
 
     val parents =
       if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
     val _ = List.app (fn (thy, r) => Context_Position.reports_global thy [r]) parents_reports;
 
     val thy = Resources.begin_theory master_dir header parents;
     val _ = Output.status [Markup.markup_only Markup.initialized];
   in thy end;
 
 fun check_root_theory node =
   let
     val master_dir = master_directory node;
     val header = #header (get_header node);
     val header_name = #1 (#name header);
     val parent =
       if header_name = Sessions.root_name then
         SOME (Thy_Info.get_theory Sessions.theory_name)
       else if member (op =) Thy_Header.ml_roots header_name then
         SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN)
       else NONE;
   in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end;
 
 fun check_theory full name node =
   is_some (Thy_Info.lookup_theory name) orelse
   null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
 
 fun last_common keywords state node_required node0 node =
   let
     fun update_flags prev (visible, initial) =
       let
         val visible' = visible andalso prev <> visible_last node;
         val initial' = initial andalso
           (case prev of
             NONE => true
           | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN);
       in (visible', initial') end;
 
     fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
       if ok then
         let
           val flags' as (visible', _) = update_flags prev flags;
           val ok' =
             (case (lookup_entry node0 command_id, opt_exec) of
               (SOME (eval0, _), SOME (eval, _)) =>
                 Command.eval_eq (eval0, eval) andalso
                   (visible' orelse node_required orelse Command.eval_running eval)
             | _ => false);
           val assign_update' = assign_update |> ok' ?
             (case opt_exec of
               SOME (eval, prints) =>
                 let
                   val command_visible = visible_command node command_id;
                   val command_overlays = overlays node command_id;
                   val command_name = the_command_name state command_id;
                 in
                   (case
                     Command.print command_visible command_overlays keywords command_name eval prints
                    of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
             | NONE => I);
         in SOME (prev, ok', flags', assign_update') end
       else NONE;
     val (common, ok, flags, assign_update') =
       iterate_entries get_common node (NONE, true, (true, true), assign_update_empty);
     val (common', flags') =
       if ok then
         let val last = Entries.get_after (get_entries node) common
         in (last, update_flags last flags) end
       else (common, flags);
   in (assign_update', common', flags') end;
 
 fun illegal_init _ = error "Illegal theory header";
 
 fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
       val command_visible = visible_command node command_id';
       val command_overlays = overlays node command_id';
       val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
       val blobs = map (resolve_blob state) blob_digests;
       val span = Lazy.force span0;
 
       val eval' =
         Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span)
           (blobs, blobs_index) command_id' span (#1 (#2 command_exec));
       val prints' =
         perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
       val init' = if command_name = Thy_Header.theoryN then NONE else init;
     in SOME (assign_update', (command_id', exec'), init') end;
 
 fun removed_execs node0 (command_id, exec_ids) =
   subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
 
 fun print_consolidation options the_command_span node_name (assign_update, node) =
   (case finished_result_theory node of
     SOME (result_id, thy) =>
       let
         val active_tasks =
           (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
             if active then NONE
             else
               (case opt_exec of
                 NONE => NONE
               | SOME (eval, _) =>
                   SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
       in
         if not active_tasks then
           let
             val consolidation =
               if Options.bool options "editor_presentation" then
                 let
                   val (_, offsets, rev_segments) =
                     iterate_entries (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) =>
                       (case opt_exec of
                         SOME (eval, _) =>
                           let
                             val command_id = Command.eval_command_id eval;
                             val span = the_command_span command_id;
 
                             val st =
                               (case try (#1 o the o the_entry node o the) prev of
                                 NONE => Toplevel.init_toplevel ()
                               | SOME prev_eval => Command.eval_result_state prev_eval);
 
                             val exec_id = Command.eval_exec_id eval;
                             val tr = Command.eval_result_command eval;
                             val st' = Command.eval_result_state eval;
 
                             val offset' = offset + the_default 0 (Command_Span.symbol_length span);
                             val offsets' = offsets
                               |> Inttab.update (command_id, offset)
                               |> Inttab.update (exec_id, offset);
                             val segments' = (span, (st, tr, st')) :: segments;
                           in SOME (offset', offsets', segments') end
                       | NONE => NONE)) node (0, Inttab.empty, []);
 
                   val adjust = Inttab.lookup offsets;
                   val segments =
                     rev rev_segments |> map (fn (span, (st, tr, st')) =>
                       {span = Command_Span.adjust_offsets adjust span,
                        prev_state = st, command = tr, state = st'});
 
                   val presentation_context: Thy_Info.presentation_context =
                    {options = options,
                     file_pos = Position.file node_name,
                     adjust_pos = Position.adjust_offsets adjust,
                     segments = segments};
                 in
                   fn _ =>
                     let
                       val _ = Output.status [Markup.markup_only Markup.consolidating];
                       val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy;
                       val _ = commit_consolidated node;
                     in Exn.release res end
                 end
               else fn _ => commit_consolidated node;
 
             val result_entry =
               (case lookup_entry node result_id of
                 NONE => err_undef "result command entry" result_id
               | SOME (eval, prints) =>
                   let
                     val print = eval |> Command.print0
                       {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
                   in (result_id, SOME (eval, print :: prints)) end);
 
             val assign_update' = assign_update |> assign_update_change result_entry;
             val node' = node |> assign_entry result_entry;
           in (assign_update', node') end
         else (assign_update, node)
       end
   | NONE => (assign_update, node));
 in
 
 fun update old_version_id new_version_id edits consolidate state =
   Runtime.exn_trace_system (fn () =>
   let
     val options = Options.default ();
     val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state;
 
     val old_version = the_version state old_version_id;
     val new_version =
       timeit "Document.edit_nodes"
         (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
 
     val consolidate = Symtab.defined (Symtab.make_set consolidate);
     val nodes = nodes_of new_version;
     val required = make_required nodes;
     val required0 = make_required (nodes_of old_version);
     val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty;
 
     val updated = timeit "Document.update" (fn () =>
       nodes |> String_Graph.schedule
         (fn deps => fn (name, node) =>
           (singleton o Future.forks)
             {name = "Document.update", group = NONE,
               deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
             (fn () =>
               timeit ("Document.update " ^ name) (fn () =>
                 Runtime.exn_trace_system (fn () =>
                   let
                     val root_theory = check_root_theory node;
                     val keywords = the_default (Session.get_keywords ()) (get_keywords node);
 
                     val maybe_consolidate = consolidate name andalso could_consolidate node;
                     val imports = map (apsnd Future.join) deps;
                     val imports_result_changed = exists (#4 o #1 o #2) imports;
                     val node_required = Symtab.defined required name;
                   in
                     if Symtab.defined edited name orelse maybe_consolidate orelse
                       visible_node node orelse imports_result_changed orelse
                       Symtab.defined required0 name <> node_required
                     then
                       let
                         val node0 = node_of old_version name;
                         val init = init_theory imports node;
                         val proper_init =
                           is_some root_theory orelse
                             check_theory false name node andalso
                             forall (fn (name, (_, node)) => check_theory true name node) imports;
 
                         val (print_execs, common, (still_visible, initial)) =
                           if imports_result_changed
                           then (assign_update_empty, NONE, (true, true))
                           else last_common keywords state node_required node0 node;
 
                         val common_command_exec =
                           (case common of
                             SOME id => (id, the_default Command.no_exec (the_entry node id))
                           | NONE => (Document_ID.none, Command.init_exec root_theory));
 
                         val (updated_execs, (command_id', exec'), _) =
                           (print_execs, common_command_exec, if initial then SOME init else NONE)
                           |> (still_visible orelse node_required) ?
                             iterate_entries_after common
                               (fn ((prev, id), _) => fn res =>
                                 if not node_required andalso prev = visible_last node then NONE
                                 else new_exec keywords state node proper_init id res) node;
 
                         val assign_update =
                           (node0, updated_execs) |-> iterate_entries_after common
                             (fn ((_, command_id0), exec0) => fn res =>
                               if is_none exec0 then NONE
                               else if assign_update_defined updated_execs command_id0 then SOME res
                               else SOME (assign_update_new (command_id0, NONE) res));
 
                         val last_exec =
                           if command_id' = Document_ID.none then NONE else SOME command_id';
                         val result =
                           if is_none last_exec orelse is_some (after_entry node last_exec) then NONE
                           else SOME (command_id', #1 exec');
 
                         val result_changed =
                           not (eq_option (Command.eval_eq o apply2 #2) (get_result node0, result));
                         val (assign_update', node') = node
                           |> assign_update_apply assign_update
                           |> set_result result
                           |> result_changed ? reset_consolidated
                           |> pair assign_update
                           |> (not result_changed andalso maybe_consolidate) ?
                               print_consolidation options the_command_span name;
 
                         val assign_result = assign_update_result assign_update';
                         val removed = maps (removed_execs node0) assign_result;
                         val _ = List.app Execution.cancel removed;
 
                         val assigned_node = SOME (name, node');
                       in ((removed, assign_result, assigned_node, result_changed), node') end
                     else (([], [], NONE, false), node)
                   end))))
       |> Future.joins |> map #1);
 
     val removed = maps #1 updated;
     val assign_result = maps #2 updated;
     val assigned_nodes = map_filter #3 updated;
 
     val state' = state
       |> define_version new_version_id new_version assigned_nodes;
 
   in (Symtab.keys edited, removed, assign_result, state') end);
 
 end;
 
 
 
 (** global state **)
 
 val global_state = Synchronized.var "Document.global_state" init_state;
 
 fun state () = Synchronized.value global_state;
 val change_state = Synchronized.change global_state;
 
 end;
diff --git a/src/Pure/Thy/export.ML b/src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML
+++ b/src/Pure/Thy/export.ML
@@ -1,73 +1,73 @@
 (*  Title:      Pure/Thy/export.ML
     Author:     Makarius
 
 Manage theory exports: compressed blobs.
 *)
 
 signature EXPORT =
 sig
   val report_export: theory -> Path.binding -> unit
   type params =
     {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
   val export_params: params -> XML.body -> unit
   val export: theory -> Path.binding -> XML.body -> unit
   val export_executable: theory -> Path.binding -> XML.body -> unit
   val export_file: theory -> Path.binding -> Path.T -> unit
   val export_executable_file: theory -> Path.binding -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
 end;
 
 structure Export: EXPORT =
 struct
 
 (* export *)
 
 fun report_export thy binding =
   let
     val theory_name = Context.theory_long_name thy;
     val (path, pos) = Path.dest_binding binding;
     val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
   in Context_Position.report_generic (Context.Theory thy) pos markup end;
 
 type params =
   {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
 fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
-   {id = Position.get_id (Position.thread_data ()),
+   {id = Position.id_of (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
     strict = strict} [body]);
 
 fun export thy binding body =
   export_params
     {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
 
 fun export_executable thy binding body =
   export_params
     {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
 
 fun export_file thy binding file =
   export thy binding [XML.Text (File.read file)];
 
 fun export_executable_file thy binding file =
   export_executable thy binding [XML.Text (File.read file)];
 
 
 (* information message *)
 
 fun markup thy path =
   let
     val thy_path = Path.basic (Context.theory_long_name thy) + path;
     val name = (Markup.nameN, Path.implode thy_path);
   in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
 
 fun message thy path =
   "See " ^ Markup.markup (markup thy path) "theory exports";
 
 end;