diff --git a/etc/options b/etc/options
--- a/etc/options
+++ b/etc/options
@@ -1,361 +1,358 @@
 (* :mode=isabelle-options: *)
 
 section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
 
 option document : string = ""
   -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
   -- "control line breaks in non-display material"
 option thy_output_cartouche : bool = false
   -- "indicate if the output should be delimited as cartouche"
 option thy_output_quotes : bool = false
   -- "indicate if the output should be delimited via double quotes"
 option thy_output_margin : int = 76
   -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
 option thy_output_source_cartouche : bool = false
   -- "print original source text rather than internal representation, preserve cartouches"
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
 
 section "Prover Output"
 
 option show_types : bool = false
   -- "show type constraints when printing terms"
 option show_sorts : bool = false
   -- "show sort constraints when printing types"
 option show_brackets : bool = false
   -- "show extra brackets when printing terms/types"
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"
 option goals_limit : int = 10
   -- "maximum number of subgoals to be printed"
 
 option names_long : bool = false
   -- "show fully qualified names"
 option names_short : bool = false
   -- "show base names only"
 option names_unique : bool = true
   -- "show partially qualified names, as required for unique name resolution"
 
 option eta_contract : bool = true
   -- "print terms in eta-contracted form"
 
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"
 
 
 section "Parallel Processing"
 
 public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
 option threads_stack_limit : real = 0.25
   -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 
 public option parallel_limit : int = 0
   -- "approximative limit for parallel tasks (0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 1
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
 option command_timing_threshold : real = 0.1
   -- "default threshold for persistent command timing (seconds)"
 
 
 section "Detail of Proof Checking"
 
 option record_proofs : int = -1
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
 option strict_facts : bool = false
   -- "force lazy facts when defined in context"
 
 
 section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
 
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
 option timeout_scale : real = 1.0
   -- "scale factor for session timeout"
 
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"
 
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
 
 section "ML System"
 
 option ML_print_depth : int = 20
   -- "ML print depth for toplevel pretty-printing"
 
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
 public option ML_exception_debugger : bool = false
   -- "ML debugger exception trace for toplevel command execution"
 
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
 
 
 section "PIDE Build"
 
 option pide_reports : bool = true
   -- "report PIDE markup"
 
 
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
 public option editor_input_delay : real = 0.3
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0
   -- "delay for machine-generated input that may outperform user edits"
 
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
 public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
 option editor_prune_size : int = 0
   -- "retained size of pruned history (delete old versions)"
 
 public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
 public option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
 public option editor_continuous_checking : bool = true
   -- "continuous checking of proof document (visible and required parts)"
 
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
 public option editor_presentation : bool = false
   -- "dynamic presentation while editing"
 
 
 section "Headless Session"
 
 option headless_consolidate_delay : real = 15
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 option headless_prune_delay : real = 60
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5
   -- "delay for theory status check during PIDE processing (seconds)"
 
 option headless_check_limit : int = 0
   -- "maximum number of theory status checks (0 = unlimited)"
 
 option headless_nodes_status_delay : real = -1
   -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
 
 option headless_watchdog_timeout : real = 600
   -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
 
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
 option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
 section "Miscellaneous Tools"
 
 public option find_theorems_limit : int = 40
   -- "limit of displayed results"
 
 public option find_theorems_tactic_limit : int = 5
   -- "limit of tactic search for 'solves' criterion"
 
 
 section "Completion"
 
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
 public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
   -- "glob patterns to ignore in file-system path completion (separated by colons)"
 
 
 section "Spell Checker"
 
 public option spell_checker : bool = true
   -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_dictionary : string = "en"
   -- "spell-checker dictionary name"
 
 public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
 public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
 section "Secure Shell"
 
 option ssh_config_dir : string = "$HOME/.ssh"
   -- "SSH configuration directory"
 
 option ssh_config_file : string = "$HOME/.ssh/config"
   -- "main SSH configuration file"
 
 option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
   -- "possible SSH identity files (separated by colons)"
 
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
 option ssh_connect_timeout : real = 60
   -- "SSH connection timeout (seconds)"
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
 option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive"
 
 
 section "Phabricator"
 
 option phabricator_version_arcanist : string = "ccd39feb6d3bbd84e122817b0d8b36284b6edd9d"
   -- "repository version for arcanist"
 
 option phabricator_version_phabricator : string = "82f98747a4e33596f8c027cb574b8ee3cb4c7d6b"
   -- "repository version for phabricator"
 
 
 section "Theory Export"
 
-option export_document : bool = false
-  -- "export document sources to Isabelle/Scala"
-
 option export_theory : bool = false
   -- "export theory content to Isabelle/Scala"
 
 option export_standard_proofs : bool = false
   -- "export standardized proof terms to Isabelle/Scala (not scalable)"
 
 option export_proofs : bool = false
   -- "export proof terms to Isabelle/Scala"
 
 option prune_proofs : bool = false
   -- "prune proof terms after export (do not store in Isabelle/ML)"
 
 
 section "Theory update"
 
 option update_inner_syntax_cartouches : bool = false
   -- "update inner syntax (types, terms, etc.) to use cartouches"
 
 option update_mixfix_cartouches : bool = false
   -- "update mixfix templates to use cartouches instead of double quotes"
 
 option update_control_cartouches : bool = false
   -- "update antiquotations to use control symbol with cartouche argument"
 
 option update_path_cartouches : bool = false
   -- "update file-system paths to use cartouches"
 
 
 section "Build Database"
 
 option build_database_server : bool = false
 option build_database_user : string = ""
 option build_database_password : string = ""
 option build_database_name : string = ""
 option build_database_host : string = ""
 option build_database_port : int = 0
 option build_database_ssh_host : string = ""
 option build_database_ssh_user : string = ""
 option build_database_ssh_port : int = 0
 
 
 section "Build Log Database"
 
 option build_log_database_user : string = ""
 option build_log_database_password : string = ""
 option build_log_database_name : string = ""
 option build_log_database_host : string = ""
 option build_log_database_port : int = 0
 option build_log_ssh_host : string = ""
 option build_log_ssh_user : string = ""
 option build_log_ssh_port : int = 0
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
 
 
 section "Isabelle/Scala/ML system channel"
 
 option system_channel_address : string = ""
 option system_channel_password : string = ""
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,489 +1,486 @@
 (*  Title:      Pure/Thy/thy_info.ML
     Author:     Markus Wenzel, TU Muenchen
 
 Global theory info database, with auto-loading according to theory and
 file dependencies.
 *)
 
 signature THY_INFO =
 sig
   type presentation_context =
     {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
       segments: Thy_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
   type context =
     {options: Options.T,
      symbols: HTML.symbols,
      bibtex_entries: string list,
      last_timing: Toplevel.transition -> Time.time}
   val use_theories: context -> string -> Path.T -> (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
 
 (** presentation of consolidated theory **)
 
 type presentation_context =
   {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     segments: Thy_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 apply_presentation (context: presentation_context) thy =
   ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
   Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
         val body = Thy_Output.present_thy options thy segments;
         val option = Present.document_option options;
       in
         if #disabled option then ()
         else
           let
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
-            val _ =
-              if Options.bool options "export_document" then
-                Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output)
-              else ();
+            val _ = Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output);
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () 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);
 
 
 (* context *)
 
 type context =
   {options: Options.T,
    symbols: HTML.symbols,
    bibtex_entries: string list,
    last_timing: Toplevel.transition -> Time.time};
 
 fun default_context (): context =
   {options = Options.default (),
    symbols = HTML.no_symbols,
    bibtex_entries = [],
    last_timing = K Time.zeroTime};
 
 
 (* scheduling loader tasks *)
 
 datatype result =
   Result of {theory: theory, exec_id: Document_ID.exec,
     present: unit -> unit, commit: unit -> unit, weight: int};
 
 fun theory_result theory =
   Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
 fun join_theory (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;
 
 fun task_finished (Task _) = false
   | task_finished (Finished _) = true;
 
 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
 
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
       Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
           val _ = Par_Exn.release_all (join_theory result);
           val _ = result_present result ();
           val _ = result_commit result ();
         in result_theory result end
     | Finished thy => thy)) #> ignore;
 
 val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   let
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
         (case task of
           Task (parents, body) =>
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = NONE,
                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
               (fn () =>
                 (case filter (not o can Future.join o #2) deps of
                   [] => body (map (result_theory o Future.join) (task_parents deps parents))
                 | bad =>
                     error
                       ("Failed to load theory " ^ quote name ^
                         " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
         | Finished theory => Future.value (theory_result theory)));
 
     val results1 = futures
       |> maps (fn future =>
           (case Future.join_result future of
             Exn.Res result => join_theory result
           | Exn.Exn exn => [Exn.Exn exn]));
 
     val results2 = futures
       |> map_filter (Exn.get_res o Future.join_result)
       |> sort result_ord
       |> Par_List.map (fn result => Exn.capture (result_present result) ());
 
     (* FIXME more precise commit order (!?) *)
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     (* FIXME avoid global Execution.reset (!??) *)
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);
 
 
 (* eval theory *)
 
 fun excursion keywords master_dir last_timing init elements =
   let
     fun prepare_span st span =
       Command_Span.content span
       |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
       |> (fn tr => Toplevel.timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
       let
         val elem = Thy_Element.map_element (prepare_span st) 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;
 
 fun eval_thy (context: context) update_time master_dir header text_pos text parents =
   let
     val {options, symbols, bibtex_entries, last_timing} = context;
     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;
 
     fun init () =
       Resources.begin_theory master_dir header parents
       |> Present.begin_theory bibtex_entries update_time
         (fn () => implode (map (HTML.present_span symbols keywords) spans));
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
         (fn () => excursion keywords master_dir last_timing init elements);
 
     fun present () =
       let
         val segments = (spans ~~ maps Toplevel.join_results results)
           |> map (fn (span, (tr, st')) => {span = span, 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, size text) 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 context initiators update_time deps text (name, pos) keywords parents =
   let
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
     val _ = Output.try_protocol_message (Markup.loading_theory name) [];
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val header = Thy_Header.make (name, pos) imports keywords;
 
     val _ =
       (imports ~~ parents) |> List.app (fn ((_, pos), thy) =>
         Context_Position.reports_global thy [(pos, Theory.get_markup thy)]);
 
     val exec_id = Document_ID.make ();
     val _ =
       Execution.running Document_ID.none exec_id [] orelse
         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
 
     val timing_start = Timing.start ();
 
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
       eval_thy context update_time 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 = present, commit = commit, weight = weight}
   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);
 
 in
 
 fun require_thys context initiators qualifier dir strs tasks =
       fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I
 and require_thy context 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' = Path.append 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 context (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) =>
                   let
                     val update_time = serial ();
                     val load =
                       load_thy context initiators update_time
                         dep text (theory_name, theory_pos) keywords;
                   in Task (parents, load) end);
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;
 
 end;
 
 
 (* use theories *)
 
 fun use_theories context qualifier master_dir imports =
   let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty
   in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
   use_theories (default_context ()) Resources.default_qualifier
     Path.current [(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);
diff --git a/src/Pure/Tools/dump.scala b/src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala
+++ b/src/Pure/Tools/dump.scala
@@ -1,510 +1,510 @@
 /*  Title:      Pure/Tools/dump.scala
     Author:     Makarius
 
 Dump cumulative PIDE session database.
 */
 
 package isabelle
 
 import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter}
 
 
 object Dump
 {
   /* aspects */
 
   sealed case class Aspect_Args(
     options: Options,
     deps: Sessions.Deps,
     progress: Progress,
     output_dir: Path,
     snapshot: Document.Snapshot,
     status: Document_Status.Node_Status)
   {
     def write_path(file_name: Path): Path =
     {
       val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
       Isabelle_System.mkdirs(path.dir)
       path
     }
 
     def write(file_name: Path, bytes: Bytes): Unit =
       Bytes.write(write_path(file_name), bytes)
 
     def write(file_name: Path, text: String): Unit =
       write(file_name, Bytes(text))
 
     def write(file_name: Path, body: XML.Body): Unit =
       using(File.writer(write_path(file_name).file))(
         writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body))
   }
 
   sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
     options: List[String] = Nil)
   {
     override def toString: String = name
   }
 
   val known_aspects: List[Aspect] =
     List(
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
             args.write(Path.explode("markup.yxml"),
               args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
         }),
       Aspect("messages", "output messages (YXML format)",
         { case args =>
             args.write(Path.explode("messages.yxml"),
               args.snapshot.messages.iterator.map(_._1).toList)
         }),
       Aspect("latex", "generated LaTeX source",
         { case args =>
             for (entry <- args.snapshot.exports if entry.name == "document.tex")
               args.write(Path.explode(entry.name), entry.uncompressed())
-        }, options = List("export_document")),
+        }),
       Aspect("theory", "foundational theory content",
         { case args =>
             for {
               entry <- args.snapshot.exports
               if entry.name.startsWith(Export_Theory.export_prefix)
             } args.write(Path.explode(entry.name), entry.uncompressed())
         }, options = List("export_theory"))
     ).sortBy(_.name)
 
   def show_aspects: String =
     cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
 
   def the_aspect(name: String): Aspect =
     known_aspects.find(aspect => aspect.name == name) getOrElse
       error("Unknown aspect " + quote(name))
 
 
   /* context and session */
 
   sealed case class Args(
     session: Headless.Session,
     snapshot: Document.Snapshot,
     status: Document_Status.Node_Status)
   {
     def print_node: String = snapshot.node_name.toString
   }
 
   object Context
   {
     def apply(
       options: Options,
       aspects: List[Aspect] = Nil,
       progress: Progress = new Progress,
       dirs: List[Path] = Nil,
       select_dirs: List[Path] = Nil,
       selection: Sessions.Selection = Sessions.Selection.empty,
       pure_base: Boolean = false,
       skip_base: Boolean = false): Context =
     {
       val session_options: Options =
       {
         val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
         val options1 =
           options0 +
             "parallel_proofs=0" +
             "completion_limit=0" +
             "editor_tracing_messages=0" +
             "editor_presentation"
         (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
       }
 
       val sessions_structure: Sessions.Structure =
         Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs).
           selection(selection)
 
       {
         val selection_size = sessions_structure.build_graph.size
         if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
       }
 
       val deps: Sessions.Deps =
         Sessions.deps(sessions_structure, progress = progress).check_errors
 
       new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps)
     }
   }
 
   class Context private(
     val options: Options,
     val progress: Progress,
     val dirs: List[Path],
     val select_dirs: List[Path],
     val pure_base: Boolean,
     val skip_base: Boolean,
     val session_options: Options,
     val deps: Sessions.Deps)
   {
     context =>
 
     def session_dirs: List[Path] = dirs ::: select_dirs
 
     def build_logic(logic: String)
     {
       Build.build_logic(options, logic, build_heap = true, progress = progress,
         dirs = session_dirs, strict = true)
     }
 
     def sessions(
       logic: String = default_logic,
       log: Logger = No_Logger): List[Session] =
     {
       /* partitions */
 
       def session_info(session_name: String): Sessions.Info =
         deps.sessions_structure(session_name)
 
       val session_graph = deps.sessions_structure.build_graph
       val all_sessions = session_graph.topological_order
 
       val afp_sessions =
         (for (name <- all_sessions if session_info(name).is_afp) yield name).toSet
 
       val afp_bulky_sessions =
         (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList
 
       val base_sessions =
         session_graph.all_preds_rev(List(logic).filter(session_graph.defined))
 
       val proof_sessions =
         session_graph.all_succs(
           for (name <- all_sessions if session_info(name).record_proofs) yield name)
 
 
       /* resulting sessions */
 
       def make_session(
         selected_sessions: List[String],
         session_logic: String = logic,
         strict: Boolean = false,
         record_proofs: Boolean = false): List[Session] =
       {
         if (selected_sessions.isEmpty && !strict) Nil
         else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
       }
 
       val PURE = isabelle.Thy_Header.PURE
 
       val base =
         if ((logic == PURE && !pure_base) || skip_base) Nil
         else make_session(base_sessions, session_logic = PURE, strict = logic == PURE)
 
       val main =
         make_session(
           session_graph.topological_order.filterNot(name =>
             afp_sessions.contains(name) ||
             base_sessions.contains(name) ||
             proof_sessions.contains(name)))
 
       val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true)
 
       val afp =
         if (afp_sessions.isEmpty) Nil
         else {
           val (part1, part2) =
           {
             val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions)
             val force_partition1 = AFP.force_partition1.filter(graph.defined)
             val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet
             graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
           }
           List(part1, part2, afp_bulky_sessions).flatMap(make_session(_))
         }
 
       proofs ::: base ::: main ::: afp
     }
 
 
     /* processed theories */
 
     private val processed_theories = Synchronized(Set.empty[String])
 
     def process_theory(theory: String): Boolean =
       processed_theories.change_result(processed => (!processed(theory), processed + theory))
 
 
     /* errors */
 
     private val errors = Synchronized(List.empty[String])
 
     def add_errors(more_errs: List[String])
     {
       errors.change(errs => errs ::: more_errs)
     }
 
     def check_errors
     {
       val errs = errors.value
       if (errs.nonEmpty) error(errs.mkString("\n\n"))
     }
   }
 
   class Session private[Dump](
     val context: Context,
     val logic: String,
     log: Logger,
     selected_sessions: List[String],
     record_proofs: Boolean)
   {
     /* resources */
 
     val options: Options =
       if (record_proofs) context.session_options + "record_proofs=2"
       else context.session_options
 
     private def deps = context.deps
     private def progress = context.progress
 
     val resources: Headless.Resources =
       Headless.Resources.make(options, logic, progress = progress, log = log,
         session_dirs = context.session_dirs,
         include_sessions = deps.sessions_structure.imports_topological_order)
 
     val used_theories: List[Document.Node.Name] =
     {
       for {
         session_name <-
           deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
         (name, theory_options) <- deps(session_name).used_theories
         if !resources.session_base.loaded_theory(name.theory)
         if {
           def warn(msg: String): Unit =
             progress.echo_warning("Skipping theory " + name + "  (" + msg + ")")
 
           val conditions =
             space_explode(',', theory_options.string("condition")).
               filter(cond => Isabelle_System.getenv(cond) == "")
           if (conditions.nonEmpty) {
             warn("undefined " + conditions.mkString(", "))
             false
           }
           else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) {
             warn("option skip_proofs")
             false
           }
           else true
         }
       } yield name
     }
 
 
     /* process */
 
     def process(process_theory: Args => Unit, unicode_symbols: Boolean = false)
     {
       val session = resources.start_session(progress = progress)
 
 
       // asynchronous consumer
 
       object Consumer
       {
         sealed case class Bad_Theory(
           name: Document.Node.Name,
           status: Document_Status.Node_Status,
           errors: List[String])
 
         private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory])
 
         private val consumer =
           Consumer_Thread.fork(name = "dump")(
             consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
               {
                 val (snapshot, status) = args
                 val name = snapshot.node_name
                 if (status.ok) {
                   try {
                     if (context.process_theory(name.theory)) {
                       process_theory(Args(session, snapshot, status))
                     }
                   }
                   catch {
                     case exn: Throwable if !Exn.is_interrupt(exn) =>
                       val msg = Exn.message(exn)
                       progress.echo("FAILED to process theory " + name)
                       progress.echo_error_message(msg)
                       consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
                   }
                 }
                 else {
                   val msgs =
                     for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
                     yield {
                       "Error" + Position.here(pos) + ":\n" +
                         XML.content(Pretty.formatted(List(tree)))
                     }
                   progress.echo("FAILED to process theory " + name)
                   msgs.foreach(progress.echo_error_message)
                   consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
                 }
                 true
               })
 
         def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit =
           consumer.send((snapshot, status))
 
         def shutdown(): List[Bad_Theory] =
         {
           consumer.shutdown()
           consumer_bad_theories.value.reverse
         }
       }
 
 
       // synchronous body
 
       try {
         val use_theories_result =
           session.use_theories(used_theories.map(_.theory),
             unicode_symbols = unicode_symbols,
             progress = progress,
             commit = Some(Consumer.apply))
 
         val bad_theories = Consumer.shutdown()
         val bad_msgs =
           bad_theories.map(bad =>
             Output.clean_yxml(
               "FAILED theory " + bad.name +
                 (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
                 (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
 
         val pending_msgs =
           use_theories_result.nodes_pending match {
             case Nil => Nil
             case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString)))
           }
 
         context.add_errors(bad_msgs ::: pending_msgs)
       }
       finally { session.stop() }
     }
   }
 
 
   /* dump */
 
   val default_output_dir: Path = Path.explode("dump")
   val default_logic: String = Thy_Header.PURE
 
   def dump(
     options: Options,
     logic: String,
     aspects: List[Aspect] = Nil,
     progress: Progress = new Progress,
     log: Logger = No_Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
     val context =
       Context(options, aspects = aspects, progress = progress, dirs = dirs,
         select_dirs = select_dirs, selection = selection)
 
     context.build_logic(logic)
 
     for (session <- context.sessions(logic = logic, log = log)) {
       session.process((args: Args) =>
         {
           progress.echo("Processing theory " + args.print_node + " ...")
           val aspect_args =
             Aspect_Args(session.options, context.deps, progress, output_dir,
               args.snapshot, args.status)
           aspects.foreach(_.operation(aspect_args))
         })
     }
 
     context.check_errors
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
     {
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
       var requirements = false
       var exclude_session_groups: List[String] = Nil
       var all_sessions = false
       var logic = default_logic
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
       var options = Options.init()
       var verbose = false
       var exclude_sessions: List[String] = Nil
 
       val getopts = Getopts("""
 Usage: isabelle dump [OPTIONS] [SESSIONS ...]
 
   Options are:
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b NAME      base logic image (default """ + isabelle.quote(default_logic) + """)
     -d DIR       include session directory
     -g NAME      select session group NAME
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
   Dump cumulative PIDE session database, with the following aspects:
 
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b:" -> (arg => logic = arg),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
       val sessions = getopts(args)
 
       val progress = new Console_Progress(verbose = verbose)
 
       val start_date = Date.now()
 
       progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date))
 
       progress.interrupt_handler {
         dump(options, logic,
           aspects = aspects,
           progress = progress,
           dirs = dirs,
           select_dirs = select_dirs,
           output_dir = output_dir,
           selection = Sessions.Selection(
             requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
             exclude_session_groups = exclude_session_groups,
             exclude_sessions = exclude_sessions,
             session_groups = session_groups,
             sessions = sessions))
       }
 
       val end_date = Date.now()
       val timing = end_date.time - start_date.time
 
       progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date))
       progress.echo(timing.message_hms + " elapsed time")
     })
 }