diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML
+++ b/src/Pure/Thy/thy_info.ML
@@ -1,450 +1,450 @@
 (*  Title:      Pure/Thy/thy_info.ML
     Author:     Makarius
 
 Global theory info database, with auto-loading according to theory and
 file dependencies, and presentation of theory documents.
 *)
 
 signature THY_INFO =
 sig
   type presentation_context =
     {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
       segments: Document_Output.segment list}
   val adjust_pos_properties: presentation_context -> Position.T -> Properties.T
   val apply_presentation: presentation_context -> theory -> unit
   val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories: Options.T -> string -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
 
 structure Thy_Info: THY_INFO =
 struct
 
 (** theory presentation **)
 
 (* hook for consolidated theory *)
 
 type presentation_context =
   {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     segments: Document_Output.segment list};
 
 fun adjust_pos_properties (context: presentation_context) pos =
   Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos;
 
 structure Presentation = Theory_Data
 (
   type T = ((presentation_context -> theory -> unit) * stamp) list;
   val empty = [];
   val extend = I;
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
 fun sequential_presentation options =
   not (Options.bool options \<^system_option>\<open>parallel_presentation\<close>);
 
 fun apply_presentation (context: presentation_context) thy =
   Par_List.map'
     {name = "apply_presentation", sequential = sequential_presentation (#options context)}
     (fn (f, _) => f context thy) (Presentation.get thy)
   |> ignore;
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
-  Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+  Theory.setup (add_presentation (fn {options, segments, ...} => fn thy =>
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
         val body = Document_Output.present_thy options thy segments;
       in
         if Options.string options "document" = "false" then ()
         else
           let
             val thy_name = Context.theory_name thy;
             val latex = Latex.isabelle_body thy_name body;
           in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end
       end));
 
 
 
 (** thy database **)
 
 (* messages *)
 
 val show_path = space_implode " via " o map quote;
 
 fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
 
 
 (* derived graph operations *)
 
 fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
   handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
 
 fun new_entry name parents entry =
   String_Graph.new_node (name, entry) #> add_deps name parents;
 
 
 (* global thys *)
 
 type deps =
  {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
   imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir_deps (d: deps option) =
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
 local
   val global_thys =
     Synchronized.var "Thy_Info.thys"
       (String_Graph.empty: (deps option * theory option) String_Graph.T);
 in
   fun get_thys () = Synchronized.value global_thys;
   fun change_thys f = Synchronized.change global_thys f;
 end;
 
 fun get_names () = String_Graph.topological_order (get_thys ());
 
 
 (* access thy *)
 
 fun lookup thys name = try (String_Graph.get_node thys) name;
 fun lookup_thy name = lookup (get_thys ()) name;
 
 fun get thys name =
   (case lookup thys name of
     SOME thy => thy
   | NONE => error ("Theory loader: nothing known about theory " ^ quote name));
 
 fun get_thy name = get (get_thys ()) name;
 
 
 (* access deps *)
 
 val lookup_deps = Option.map #1 o lookup_thy;
 
 val master_directory = master_dir_deps o #1 o get_thy;
 
 
 (* access theory *)
 
 fun lookup_theory name =
   (case lookup_thy name of
     SOME (_, SOME theory) => SOME theory
   | _ => NONE);
 
 fun get_theory name =
   (case lookup_theory name of
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
 val get_imports = Resources.imports_of o get_theory;
 
 
 
 (** thy operations **)
 
 (* remove *)
 
 fun remove name thys =
   (case lookup thys name of
     NONE => thys
   | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name)
   | SOME _ =>
       let
         val succs = String_Graph.all_succs thys [name];
         val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
       in fold String_Graph.del_node succs thys end);
 
 val remove_thy = change_thys o remove;
 
 
 (* update *)
 
 fun update deps theory thys =
   let
     val name = Context.theory_long_name theory;
     val parents = map Context.theory_long_name (Theory.parents_of theory);
 
     val thys' = remove name thys;
     val _ = map (get thys') parents;
   in new_entry name parents (SOME deps, SOME theory) thys' end;
 
 fun update_thy deps theory = change_thys (update deps theory);
 
 
 (* scheduling loader tasks *)
 
 datatype result =
   Result of {theory: theory, exec_id: Document_ID.exec,
     present: (unit -> unit) option, commit: unit -> unit};
 
 fun theory_result theory =
   Result {theory = theory, exec_id = Document_ID.none, present = NONE, commit = I};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 
 fun consolidate_theory (Exn.Exn exn) = [Exn.Exn exn]
   | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
       let
         val _ = Execution.join [exec_id];
         val res = Exn.capture Thm.consolidate_theory theory;
         val exns = maps Task_Queue.group_status (Execution.peek exec_id);
       in res :: map Exn.Exn exns end;
 
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;
 
 val schedule_theories = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   let
     fun join_parents deps name parents =
       (case map #1 (filter (not o can Future.join o #2) deps) of
         [] => map (result_theory o Future.join o the o AList.lookup (op =) deps) parents
       | bad =>
           error ("Failed to load theory " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")"));
 
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
         (case task of
           Task (parents, body) =>
             if Multithreading.max_threads () > 1 then
               (singleton o Future.forks)
                 {name = "theory:" ^ name, group = NONE,
                   deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
                 (fn () => body (join_parents deps name parents))
             else
               Future.value_result (Exn.capture (fn () => body (join_parents deps name parents)) ())
         | Finished theory => Future.value (theory_result theory)));
 
     val results1 = futures |> maps (consolidate_theory o Future.join_result);
 
     val results2 = futures
       |> map_filter (Option.mapPartial result_present o Exn.get_res o Future.join_result)
       |> Par_List.map'
           {name = "present", sequential = sequential_presentation (Options.default ())}
           (fn present => Exn.capture present ());
 
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
   in ignore (Par_Exn.release_all (results1 @ results2 @ results3 @ results4)) end);
 
 
 (* eval theory *)
 
 fun eval_thy options master_dir header text_pos text parents =
   let
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
 
     val text_id = Position.copy_id text_pos Position.none;
 
     fun init () = Resources.begin_theory master_dir header parents;
 
     fun excursion () =
       let
         fun element_result span_elem (st, _) =
           let
             fun prepare span =
               let
                 val tr =
                   Position.setmp_thread_data text_id
                     (fn () => Command.read_span keywords st master_dir init span) ();
               in Toplevel.timing (Resources.last_timing tr) tr end;
             val elem = Thy_Element.map_element prepare span_elem;
             val (results, st') = Toplevel.element_result keywords elem st;
             val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
           in (results, (st', pos')) end;
 
         val (results, (end_state, end_pos)) =
           fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
 
         val thy = Toplevel.end_theory end_pos end_state;
       in (results, thy) end;
 
     val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion;
 
     fun present () =
       let
         val segments =
           (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) =>
             {span = span, prev_state = st, command = tr, state = st'});
         val context: presentation_context =
           {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
       in apply_presentation context thy end;
 
   in (thy, present) end;
 
 
 (* require_thy -- checking database entries wrt. the file-system *)
 
 local
 
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
 fun load_thy options initiators deps text (name, header_pos) keywords parents =
   let
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
 
     val exec_id = Document_ID.make ();
     val id = Document_ID.print exec_id;
     val put_id = Position.put_id id;
     val _ =
       Execution.running Document_ID.none exec_id [] orelse
         raise Fail ("Failed to register execution: " ^ id);
 
     val text_pos = put_id (Path.position thy_path);
     val text_props = Position.properties_of text_pos;
 
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
     val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]];
 
     val _ =
       Position.setmp_thread_data (Position.id_only id) (fn () =>
         (parents, map #2 imports) |> ListPair.app (fn (thy, pos) =>
           Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) ();
 
     val timing_start = Timing.start ();
 
     val header = Thy_Header.make (name, put_id header_pos) imports keywords;
     val (theory, present) =
       eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
     val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
   in Result {theory = theory, exec_id = exec_id, present = SOME present, commit = commit} end;
 
 fun check_thy_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   | NONE =>
       let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   | SOME (SOME {master, ...}) =>
       let
         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
           keywords = keywords'} = Resources.check_thy dir name;
         val deps' = SOME (make_deps master' imports', text');
         val current =
           #2 master = #2 master' andalso
             (case lookup_theory name of
               NONE => false
             | SOME theory => Resources.loaded_files_current theory);
       in (current, deps', theory_pos', imports', keywords') end);
 
 fun task_finished (Task _) = false
   | task_finished (Finished _) = true;
 
 in
 
 fun require_thys options initiators qualifier dir strs tasks =
       fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I
 and require_thy options initiators qualifier dir (s, require_pos) tasks =
   let
     val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   in
     (case try (String_Graph.get_node tasks) theory_name of
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
           val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name
             handle ERROR msg =>
               cat_error msg
                 ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
           val qualifier' = Resources.theory_qualifier theory_name;
           val dir' = dir + master_dir_deps (Option.map #1 deps);
 
           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
             require_thys options (theory_name :: initiators) qualifier' dir' imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
             if all_current then Finished (get_theory theory_name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
                   Task (parents,
                     load_thy options initiators dep text (theory_name, theory_pos) keywords));
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;
 
 end;
 
 
 (* use theories *)
 
 fun use_theories options qualifier imports =
   schedule_theories (#2 (require_thys options [] qualifier Path.current imports String_Graph.empty));
 
 fun use_thy name =
   use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
 
 fun script_thy pos txt thy =
   let
     val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
     val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
   in Toplevel.end_theory end_pos end_state end;
 
 
 (* register theory *)
 
 fun register_thy theory =
   let
     val name = Context.theory_long_name theory;
     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
     val imports = Resources.imports_of theory;
   in
     change_thys (fn thys =>
       let
         val thys' = remove name thys;
         val _ = writeln ("Registering theory " ^ quote name);
       in update (make_deps master imports) theory thys' end)
   end;
 
 
 (* finish all theories *)
 
 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
 
 end;
 
 fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);