diff --git a/etc/options b/etc/options
--- a/etc/options
+++ b/etc/options
@@ -1,387 +1,387 @@
 (* :mode=isabelle-options: *)
 
 section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
 
 option document : string = "" (standard "true")
   -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
 option document_output : string = "" (standard "output")
   -- "document output directory"
 option document_echo : bool = false
   -- "inform about document file names during session presentation"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
 option document_bibliography : bool = false
   -- "explicitly enable use of bibtex (default: according to presence of root.bib)"
 option document_build : string = "lualatex" (standard "build")
   -- "document build engine (e.g. build, lualatex, pdflatex)"
 option document_logo : string = "" (standard "_")
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
 option document_heading_prefix : string = "isamarkup" (standard)
   -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
 option document_comment_latex : bool = false
   -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version"
 
 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 show_states : bool = false
   -- "show toplevel states even if outside of interactive mode"
 
 
 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 and Timing"
 
 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)"
 
 public option timeout_scale : real = 1.0
   -- "scale factor for timeout in Isabelle/ML and session build"
 
 
 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_build : bool = true
   -- "observe timeout for session build"
 
 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 = "" (standard "time")
   -- "ML profiling (possible values: time, time_thread, allocations)"
 
 option system_log : string = "" (standard "-")
   -- "output for system messages (log file or \"-\" for console progress)"
 
 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
   -- "prefer native 64bit platform (change requires restart)"
 
 public option ML_system_apple : bool = true
   -- "prefer native Apple/ARM64 platform (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 (in ML)"
 
 option build_pide_reports : bool = true
   -- "report PIDE markup (in batch build)"
 
+option pide_presentation : bool = false
+  -- "presentation of consolidated theories in PIDE"
+
 
 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.2
   -- "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 (OpenSSH)"
 
 public option ssh_batch_mode : bool = true
   -- "enable SSH batch mode (no user interaction)"
 
 public option ssh_multiplexing : bool = true
   -- "enable multiplexing of SSH sessions (ignored on Windows)"
 
 public option ssh_compression : bool = true
   -- "enable SSH compression"
 
 public option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds, ignore value < 0)"
 
 public option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive (ignore value < 0)"
 
 
 section "Phabricator"
 
 option phabricator_version_arcanist : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a"
   -- "repository version for arcanist"
 
 option phabricator_version_phabricator : string = "193798385bd3a7f72dca255e44f8112f4f8fc155"
   -- "repository version for phabricator"
 
 
 section "Theory Export"
 
 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 = ""
 
 
 section "Bash process execution server"
 
 option bash_process_debugging : bool = false
 option bash_process_address : string = ""
 option bash_process_password : string = ""
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,506 +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 ->
+  val print: Keyword.keywords -> bool -> (string * string list) list -> 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_local () =
       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_remote () =
       let
         val text = Bytes.content (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_local ()
       | SOME (Url.File _) => read_local ()
       | _ => read_remote ());
 
     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.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 core_range = Token.core_range_of span;
     val tr =
       if exists #1 token_reports
       then Toplevel.malformed (#1 core_range) "Malformed command syntax"
       else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span);
     val _ =
       if Toplevel.is_ignored tr orelse Toplevel.is_malformed tr then ()
       else Position.report (#1 core_range) (Markup.command_span (Toplevel.name_of tr));
   in tr 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 = Toplevel.make_state opt_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;
 fun print_equiv (name', args') (Print {name, args, ...}) = name' = name andalso args' = args;
 
 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 =
+fun print keywords visible overlays 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 (print_equiv (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
+      if visible then
+        fold (fn (name, _) => cons (name, [])) print_functions 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");
+  pri <= 0 orelse (Future.enabled () andalso Options.default_bool \<^system_option>\<open>parallel_print\<close>);
 
 fun print_function name f =
   Synchronized.change print_functions (fn funs =>
    (if name = "" then error "Unnamed print function"
     else if AList.defined (op =) funs name then
       warning ("Redefining command print function: " ^ quote name)
     else ();
     AList.update (op =) (name, f) funs));
 
 fun no_print_function name =
   Synchronized.change print_functions (filter_out (equal name o #1));
 
 end;
 
 
 (* 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;
 
 
 (* common print functions *)
 
 val _ =
   Command.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 _ =
   Command.print_function "print_state"
     (fn {keywords, command_name, ...} =>
-      if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name
+      if Options.default_bool \<^system_option>\<open>editor_output_state\<close>
+        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);
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,934 +1,931 @@
 (*  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 read_header node span =
   let
-    val {header, errors, ...} = get_header node;
-    val _ =
-      if null errors then ()
-      else
-        cat_lines errors |>
-        (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;
+    val (name, imports0) =
+      (case get_header node of
+        {errors = [], header = {name = (name, _), imports, ...}, ...} => (name, imports)
+      | {errors, ...} =>
+          cat_lines errors |>
+          (case Position.id_of (Position.thread_data ()) of
+            NONE => I
+          | SOME id => Protocol_Message.command_positions_yxml id)
+          |> error);
+    val {name = (_, pos), imports = imports1, keywords} = Thy_Header.read_tokens Position.none span;
+    val imports = (map #1 imports0 ~~ map #2 imports1) handle ListPair.UnequalLengths => imports0;
+  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 command_overlays = Inttab.lookup_list o #overlays o get_perspective;
+val command_visible = 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;
 
 fun get_consolidated (Node {consolidated, ...}) = consolidated;
 
 val reset_consolidated =
   map_node (fn (header, keywords, perspective, entries, result, _) =>
     (header, keywords, perspective, entries, result, Lazy.lazy I));
 
 fun could_consolidate node =
   not (Lazy.is_finished (get_consolidated 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;
 
 
 (* outer syntax keywords *)
 
 val pure_keywords = Thy_Header.get_keywords o Theory.get_pure;
 
 fun theory_keywords name =
   (case Thy_Info.lookup_theory name of
     SOME thy => Thy_Header.get_keywords thy
   | NONE => Keyword.empty_keywords);
 
 fun node_keywords name node =
   (case node of
     Node {keywords = SOME keywords, ...} => keywords
   | _ => theory_keywords name);
 
 
 (* 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 (node_keywords name o get_node nodes o #1) (#imports header);
         val keywords = Library.foldl Keyword.merge_keywords (pure_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});
 
 
 (* 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
                               SOME (Url.File path) => Markup.path (Path.implode path)
                             | _ => 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);
                       fun reports (Exn.Res {file_node, ...}) = [(pos, Markup.path file_node)]
                         | reports _ = [];
                     in Position.reports (maps reports 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' =
       Inttab.build (versions' |>
         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' =
       Symtab.build (commands' |>
         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 delay = seconds (Options.default_real \<^system_option>\<open>editor_execution_delay\<close>);
 
       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 Thy_Info.defined_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) : 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) =
+fun assign_update_new upd (tab: assign_update) : 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.make_state NONE;
 
     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.make_state NONE
               | 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 =
+fun get_special_parent node =
   let
     val master_dir = master_directory node;
-    val header = #header (get_header node);
-    val header_name = #1 (#name header);
+    val header as {name = (name, _), ...} = #header (get_header node);
     val parent =
-      if header_name = Sessions.root_name then
+      if name = Sessions.root_name then
         SOME (Thy_Info.get_theory Sessions.theory_name)
-      else if member (op =) Thy_Header.ml_roots header_name then
+      else if member (op =) Thy_Header.ml_roots 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 =
   Thy_Info.defined_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 =
+fun last_common keywords the_command_name 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);
+          | SOME command_id => the_command_name 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;
-                  val command_print =
-                    Command.print command_visible command_overlays keywords command_name eval prints;
+                  val visible = command_visible node command_id;
+                  val overlays = command_overlays node command_id;
+                  val command_name = the_command_name command_id;
                 in
-                  (case command_print of
+                  (case Command.print keywords visible overlays 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 visible = command_visible node command_id';
+      val overlays = command_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 prints' = perhaps (Command.print keywords visible overlays 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) =>
-      timeit "Document.print_consolidation" (fn () =>
-        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
-              fun commit_consolidated () =
-                (Lazy.force (get_consolidated node);
-                 Output.status [Markup.markup_only Markup.consolidated]);
-              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.make_state NONE
-                                | 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;
+fun finished_eval node =
+  let
+    val active =
+      (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active =>
+        if active then NONE
+        else
+          (case opt_exec of
+            NONE => SOME true
+          | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval])))));
+  in not active end;
 
-                              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'});
+fun presentation_context options the_command_span node_name node : Thy_Info.presentation_context =
+  let
+    val (_, offsets, rev_segments) =
+      (node, (0, Inttab.empty, [])) |-> iterate_entries
+        (fn ((prev, id), 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 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 ();
-                      in Exn.release res end
-                  end
-                else fn _ => commit_consolidated ();
+                val st =
+                  (case try (#1 o the o the_entry node o the) prev of
+                    NONE => Toplevel.make_state NONE
+                  | SOME prev_eval => Command.eval_result_state prev_eval);
 
-              val result_entry =
-                (case lookup_entry node result_id of
-                  NONE => err_undef "result command entry" result_id
-                | SOME (eval, prints) =>
+                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 => raise Fail ("Unassigned exec " ^ Value.print_int id)));
+
+    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'});
+  in
+   {options = options,
+    file_pos = Position.file node_name,
+    adjust_pos = Position.adjust_offsets adjust,
+    segments = segments}
+  end;
+
+fun print_consolidation options the_command_span node_name (assign_update, node) =
+  timeit "Document.print_consolidation" (fn () =>
+    (case finished_result_theory node of
+      SOME (result_id, thy) =>
+        if finished_eval node then
+          let
+            fun commit_consolidated () =
+              (Lazy.force (get_consolidated node);
+               Output.status [Markup.markup_only Markup.consolidated]);
+            val consolidation =
+              if Options.bool options \<^system_option>\<open>pide_presentation\<close> then
+                let val context = presentation_context options the_command_span node_name node in
+                  fn _ =>
                     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 _ = Output.status [Markup.markup_only Markup.consolidating];
+                      val res = Exn.capture (Thy_Info.apply_presentation context) thy;
+                      val _ = commit_consolidated ();
+                    in Exn.release res end
+                end
+              else fn _ => commit_consolidated ();
 
-              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));
+            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)
+    | 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_name = #1 o the_command state;
     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 = Symtab.build (edits |> fold (fn (name, _) => Symtab.update (name, ())));
+    val edited = Symtab.build (edits |> fold (Symtab.insert_set o #1));
 
     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 special_parent = get_special_parent node;
                     val keywords = node_keywords name 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
+                          is_some special_parent 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;
+                          else last_common keywords the_command_name 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));
+                          | NONE => (Document_ID.none, Command.init_exec special_parent));
 
                         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/document_output.ML b/src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML
+++ b/src/Pure/Thy/document_output.ML
@@ -1,589 +1,590 @@
 (*  Title:      Pure/Thy/document_output.ML
     Author:     Makarius
 
 Theory document output.
 *)
 
 signature DOCUMENT_OUTPUT =
 sig
   val document_reports: Input.source -> Position.report list
   val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text
   val document_output: {markdown: bool, markup: Latex.text -> Latex.text} ->
     (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val output_token: Proof.context -> Token.T -> Latex.text
   val output_source: Proof.context -> string -> Latex.text
   type segment =
     {span: Command_Span.span, command: Toplevel.transition,
      prev_state: Toplevel.state, state: Toplevel.state}
-  val present_thy: Options.T -> Keyword.keywords -> segment list -> Latex.text
+  val present_thy: Options.T -> Keyword.keywords -> string -> segment list -> Latex.text
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val isabelle: Proof.context -> Latex.text -> Latex.text
   val isabelle_typewriter: Proof.context -> Latex.text -> Latex.text
   val typewriter: Proof.context -> string -> Latex.text
   val verbatim: Proof.context -> string -> Latex.text
   val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
   val pretty: Proof.context -> Pretty.T -> Latex.text
   val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
   val pretty_items: Proof.context -> Pretty.T list -> Latex.text
   val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
     Pretty.T list -> Latex.text
   val antiquotation_pretty:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_raw:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_raw_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_verbatim:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
   val antiquotation_verbatim_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
 end;
 
 structure Document_Output: DOCUMENT_OUTPUT =
 struct
 
 (* output document source *)
 
 fun document_reports txt =
   let val pos = Input.pos_of txt in
     [(pos, Markup.language_document (Input.is_delimited txt)),
      (pos, Markup.plain_text)]
   end;
 
 fun output_comment ctxt (kind, syms) =
   (case kind of
     Comment.Comment =>
       Input.cartouche_content syms
       |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
           {markdown = false}
       |> XML.enclose "%\n\\isamarkupcmt{" "%\n}"
   | Comment.Cancel =>
       Symbol_Pos.cartouche_content syms
       |> Latex.symbols_output
       |> XML.enclose "%\n\\isamarkupcancel{" "}"
   | Comment.Latex => Latex.symbols (Symbol_Pos.cartouche_content syms)
   | Comment.Marker => [])
 and output_comment_document ctxt (comment, syms) =
   (case comment of
     SOME kind => output_comment ctxt (kind, syms)
   | NONE => Latex.symbols syms)
 and output_document_text ctxt syms =
   Comment.read_body syms |> maps (output_comment_document ctxt)
 and output_document ctxt {markdown} source =
   let
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
 
     val output_antiquotes =
       maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt);
 
     fun output_line line =
       (if Markdown.line_is_item line then Latex.string "\\item " else []) @
         output_antiquotes (Markdown.line_content line);
 
     fun output_block (Markdown.Par lines) =
           separate (XML.Text "\n") (map (Latex.block o output_line) lines)
       | output_block (Markdown.List {kind, body, ...}) =
           Latex.environment (Markdown.print_kind kind) (output_blocks body)
     and output_blocks blocks =
       separate (XML.Text "\n\n") (map (Latex.block o output_block) blocks);
   in
     if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
     then
       let
         val ants = Antiquote.parse_comments pos syms;
         val reports = Antiquote.antiq_reports ants;
         val blocks = Markdown.read_antiquotes ants;
         val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
       in output_blocks blocks end
     else
       let
         val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
         val reports = Antiquote.antiq_reports ants;
         val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
       in output_antiquotes ants end
   end;
 
 fun document_output {markdown, markup} (loc, txt) =
   let
     fun output st =
       let
         val ctxt = Toplevel.presentation_context st;
         val _ = Context_Position.reports ctxt (document_reports txt);
       in txt |> output_document ctxt {markdown = markdown} |> markup end;
   in
     Toplevel.present (fn st =>
       (case loc of
         NONE => output st
       | SOME (_, pos) =>
           error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
     Toplevel.present_local_theory loc output
   end;
 
 
 (* output tokens with formal comments *)
 
 local
 
 val output_symbols_antiq =
   (fn Antiquote.Text syms => Latex.symbols_output syms
     | Antiquote.Control {name = (name, _), body, ...} =>
         Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) @
           Latex.symbols_output body
     | Antiquote.Antiq {body, ...} =>
         XML.enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.symbols_output body));
 
 fun output_comment_symbols ctxt {antiq} (comment, syms) =
   (case (comment, antiq) of
     (NONE, false) => Latex.symbols_output syms
   | (NONE, true) =>
       Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms
       |> maps output_symbols_antiq
   | (SOME comment, _) => output_comment ctxt (comment, syms));
 
 fun output_body ctxt antiq bg en syms =
   Comment.read_body syms
   |> maps (output_comment_symbols ctxt {antiq = antiq})
   |> XML.enclose bg en;
 
 in
 
 fun output_token ctxt tok =
   let
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
   in
     (case Token.kind_of tok of
       Token.Comment NONE => []
     | Token.Comment (SOME Comment.Marker) => []
     | Token.Command => output false "\\isacommand{" "}"
     | Token.Keyword =>
         if Symbol.is_ascii_identifier (Token.content_of tok)
         then output false "\\isakeyword{" "}"
         else output false "" ""
     | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
     | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
     | Token.Control control => output_body ctxt false "" "" (Antiquote.control_symbols control)
     | _ => output false "" "")
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 fun output_source ctxt s =
   output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
 
 fun check_comments ctxt =
   Comment.read_body #> List.app (fn (comment, syms) =>
     let
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
           Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
       val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
 end;
 
 
 
 (** present theory source **)
 
 (* presentation tokens *)
 
 datatype token =
     Ignore
   | Token of Token.T
   | Output of Latex.text;
 
 fun token_with pred (Token tok) = pred tok
   | token_with _ _ = false;
 
 val white_token = token_with Document_Source.is_white;
 val white_comment_token = token_with Document_Source.is_white_comment;
 val blank_token = token_with Token.is_blank;
 val newline_token = token_with Token.is_newline;
 
 fun present_token ctxt tok =
   (case tok of
     Ignore => []
   | Token tok => output_token ctxt tok
   | Output output => output);
 
 
 (* command spans *)
 
 type command = string * Position.T;  (*name, position*)
 type source = (token * (string * int)) list;  (*token, markup flag, meta-comment depth*)
 
 datatype span = Span of command * (source * source * source * source) * bool;
 
 fun make_span cmd src =
   let
     fun chop_newline (tok :: toks) =
           if newline_token (fst tok) then ([tok], toks, true)
           else ([], tok :: toks, false)
       | chop_newline [] = ([], [], false);
     val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
       src
       |> chop_prefix (white_token o fst)
       ||>> chop_suffix (white_token o fst)
       ||>> chop_prefix (white_comment_token o fst)
       ||> chop_newline;
   in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
 
 
 (* present spans *)
 
 local
 
 fun err_bad_nesting here =
   error ("Bad nesting of commands in presentation" ^ here);
 
 fun edge which f (x: string option, y) =
   if x = y then I
   else (case which (x, y) of NONE => I | SOME txt => fold cons (Latex.string (f txt)));
 
 val markup_tag = YXML.output_markup o Markup.latex_tag;
 val markup_delim = YXML.output_markup o Markup.latex_delim;
 val bg_delim = #1 o markup_delim;
 val en_delim = #2 o markup_delim;
 
 val begin_tag = edge #2 (#1 o markup_tag);
 val end_tag = edge #1 (#2 o markup_tag);
 fun open_delim delim e = edge #2 bg_delim e #> delim #> edge #2 en_delim e;
 fun close_delim delim e = edge #1 bg_delim e #> delim #> edge #1 en_delim e;
 
 fun document_tag cmd_pos state state' tagging_stack =
   let
     val ctxt' = Toplevel.presentation_context state';
     val nesting = Toplevel.level state' - Toplevel.level state;
 
     val (tagging, taggings) = tagging_stack;
     val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
 
     val tagging_stack' =
       if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
       else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
       else
         (case drop (~ nesting - 1) taggings of
           tg :: tgs => (tg, tgs)
         | [] => err_bad_nesting (Position.here cmd_pos));
   in (tag', tagging_stack') end;
 
 fun read_tag s =
   (case space_explode "%" s of
     ["", b] => (SOME b, NONE)
   | [a, b] => (NONE, SOME (a, b))
   | _ => error ("Bad document_tags specification: " ^ quote s));
 
 in
 
 fun make_command_tag options keywords =
   let
     val document_tags =
       map read_tag (space_explode "," (Options.string options \<^system_option>\<open>document_tags\<close>));
     val document_tags_default = map_filter #1 document_tags;
     val document_tags_command = map_filter #2 document_tags;
   in
     fn name => fn st => fn st' => fn active_tag =>
       let
         val keyword_tags =
           if Keyword.is_theory_end keywords name andalso Toplevel.is_end_theory st' then ["theory"]
           else Keyword.command_tags keywords name;
         val command_tags =
           the_list (AList.lookup (op =) document_tags_command name) @
           keyword_tags @ document_tags_default;
         val active_tag' =
           (case command_tags of
             default_tag :: _ => SOME default_tag
           | [] =>
               if Keyword.is_vacuous keywords name andalso Toplevel.is_proof st
               then active_tag else NONE);
       in active_tag' end
   end;
 
 fun present_span command_tag span state state'
     (tagging_stack, active_tag, newline, latex, present_cont) =
   let
     val ctxt' = Toplevel.presentation_context state';
     val present = fold (fn (tok, (flag, 0)) =>
         fold cons (present_token ctxt' tok)
         #> fold cons (Latex.string flag)
       | _ => I);
 
     val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
 
     val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
     val active_tag' =
       if is_some tag' then Option.map #1 tag'
       else command_tag cmd_name state state' active_tag;
     val edge = (active_tag, active_tag');
 
     val newline' =
       if is_none active_tag' then span_newline else newline;
 
     val latex' =
       latex
       |> end_tag edge
       |> close_delim (fst present_cont) edge
       |> snd present_cont
       |> open_delim (present (#1 srcs)) edge
       |> begin_tag edge
       |> present (#2 srcs);
     val present_cont' =
       if newline then (present (#3 srcs), present (#4 srcs))
       else (I, present (#3 srcs) #> present (#4 srcs));
   in (tagging_stack', active_tag', newline', latex', present_cont') end;
 
 fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
   if not (null tags) then err_bad_nesting " at end of theory"
   else
     latex
     |> end_tag (active_tag, NONE)
     |> close_delim (fst present_cont) (active_tag, NONE)
     |> snd present_cont;
 
 end;
 
 
 (* present_thy *)
 
 type segment =
   {span: Command_Span.span, command: Toplevel.transition,
    prev_state: Toplevel.state, state: Toplevel.state};
 
 local
 
 val markup_true = "\\isamarkuptrue%\n";
 val markup_false = "\\isamarkupfalse%\n";
 
 fun command_output output tok =
   if Token.is_command tok then SOME (Token.put_output output tok) else NONE;
 
 fun segment_content (segment: segment) =
   let val toks = Command_Span.content (#span segment) in
     (case Toplevel.output_of (#state segment) of
       NONE => toks
     | SOME output => map_filter (command_output output) toks)
   end;
 
 fun output_command keywords = Scan.some (fn tok =>
   if Token.is_command tok then
     let
       val name = Token.content_of tok;
       val is_document = Keyword.is_document keywords name;
       val is_document_raw = Keyword.is_document_raw keywords name;
       val flag = if is_document andalso not is_document_raw then markup_true else "";
     in
       if is_document andalso is_some (Token.get_output tok)
       then SOME ((name, Token.pos_of tok), the (Token.get_output tok), flag)
       else NONE
     end
   else NONE);
 
 val opt_newline = Scan.option (Scan.one Token.is_newline);
 
 val ignore =
   Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
     >> pair (d + 1)) ||
   Scan.depend (fn d => Scan.one Token.is_end_ignore --|
     (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     >> pair (d - 1));
 
 in
 
-fun present_thy options keywords (segments: segment list) =
+fun present_thy options keywords thy_name (segments: segment list) =
   let
     (* tokens *)
 
     val ignored = Scan.state --| ignore
       >> (fn d => [(NONE, (Ignore, ("", d)))]);
 
     val output = Scan.peek (fn d =>
       Document_Source.improper |-- output_command keywords --| Document_Source.improper_end
         >> (fn (kind, body, flag) => [(SOME kind, (Output body, (flag, d)))]));
 
     val command = Scan.peek (fn d =>
       Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
       Scan.one Token.is_command --| Document_Source.annotation
       >> (fn (cmd_mod, cmd) =>
         map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @
           [(SOME (Token.content_of cmd, Token.pos_of cmd),
             (Token cmd, (markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>
       Scan.one Document_Source.is_black_comment >> (fn tok => [(NONE, (Token tok, ("", d)))]));
 
     val other = Scan.peek (fn d =>
        Parse.not_eof >> (fn tok => [(NONE, (Token tok, ("", d)))]));
 
     val tokens = ignored || output || command || cmt || other;
 
 
     (* spans *)
 
     val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false;
     val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof;
 
     val cmd = Scan.one (is_some o fst);
     val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
 
     val white_comments = Scan.many (white_comment_token o fst o snd);
     val blank = Scan.one (blank_token o fst o snd);
     val newline = Scan.one (newline_token o fst o snd);
     val before_cmd =
       Scan.option (newline -- white_comments) --
       Scan.option (newline -- white_comments) --
       Scan.option (blank -- white_comments) -- cmd;
 
     val span =
       Scan.repeat non_cmd -- cmd --
         Scan.repeat (Scan.unless before_cmd non_cmd) --
         Scan.option (newline >> (single o snd))
       >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
     val spans = segments
       |> maps segment_content
       |> drop_suffix Token.is_space
       |> Source.of_list
       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
       |> Source.source stopper (Scan.error (Scan.bulk span))
       |> Source.exhaust;
 
     val command_results =
       segments |> map_filter (fn {command, state, ...} =>
         if Toplevel.is_ignored command then NONE else SOME (command, state));
 
 
     (* present commands *)
 
     val command_tag = make_command_tag options keywords;
 
     fun present_command tr span st st' =
       Toplevel.setmp_thread_position tr (present_span command_tag span st st');
 
     fun present _ [] = I
       | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   in
     if length command_results = length spans then
       (([], []), NONE, true, [], (I, I))
       |> present (Toplevel.make_state NONE) (spans ~~ command_results)
       |> present_trailer
       |> rev
+      |> Latex.isabelle_body thy_name
     else error "Messed-up outer syntax for presentation"
   end;
 
 end;
 
 
 
 (** standard output operations **)
 
 (* pretty printing *)
 
 fun pretty_term ctxt t =
   Syntax.pretty_term (Proof_Context.augment t ctxt) t;
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 
 (* default output *)
 
 fun isabelle ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
   then Latex.environment "isabelle" body
   else Latex.macro "isa" body;
 
 fun isabelle_typewriter ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
   then Latex.environment "isabellett" body
   else Latex.macro "isatt" body;
 
 fun typewriter ctxt s =
   isabelle_typewriter ctxt (Latex.string (Latex.output_ascii s));
 
 fun verbatim ctxt =
   if Config.get ctxt Document_Antiquotation.thy_output_display
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
   else split_lines #> map (typewriter ctxt #> Latex.block) #> separate (XML.Text "\\isanewline%\n");
 
 fun token_source ctxt {embedded} tok =
   if Token.is_kind Token.Cartouche tok andalso embedded andalso
     not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
   then Token.content_of tok
   else Token.unparse tok;
 
 fun is_source ctxt =
   Config.get ctxt Document_Antiquotation.thy_output_source orelse
   Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
 
 fun source ctxt embedded =
   Token.args_of_src
   #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
   #> space_implode " "
   #> output_source ctxt
   #> isabelle ctxt;
 
 fun pretty ctxt =
   Document_Antiquotation.output ctxt #> Latex.string #> isabelle ctxt;
 
 fun pretty_source ctxt embedded src prt =
   if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
 
 fun pretty_items ctxt =
   map (Document_Antiquotation.output ctxt #> XML.Text) #>
   separate (XML.Text "\\isasep\\isanewline%\n") #> isabelle ctxt;
 
 fun pretty_items_source ctxt embedded src prts =
   if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
 
 
 (* antiquotation variants *)
 
 local
 
 fun gen_setup name embedded =
   if embedded
   then Document_Antiquotation.setup_embedded name
   else Document_Antiquotation.setup name;
 
 fun gen_antiquotation_pretty name embedded scan f =
   gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
 
 fun gen_antiquotation_pretty_source name embedded scan f =
   gen_setup name embedded scan
     (fn {context = ctxt, source = src, argument = x} =>
       pretty_source ctxt {embedded = embedded} src (f ctxt x));
 
 fun gen_antiquotation_raw name embedded scan f =
   gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
 
 fun gen_antiquotation_verbatim name embedded scan f =
   gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
 
 in
 
 fun antiquotation_pretty name = gen_antiquotation_pretty name false;
 fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
 
 fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
 fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
 
 fun antiquotation_raw name = gen_antiquotation_raw name false;
 fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
 
 fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
 fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
 
 end;
 
 end;
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,463 +1,461 @@
 (*  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 defined_theory: string -> bool
   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 ->
     (theory * Document_Output.segment list) list
   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) @
   filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.get_props pos);
 
 structure Presentation = Theory_Data
 (
   type T = ((presentation_context -> theory -> unit) * stamp) list;
   val empty = [];
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
 fun apply_presentation (context: presentation_context) thy =
   ignore (Par_List.map (fn (f, _) => f context thy) (Presentation.get thy));
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
   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_Header.get_keywords thy) segments;
+        val keywords = Thy_Header.get_keywords thy;
+        val thy_name = Context.theory_name thy;
+        val latex = Document_Output.present_thy options keywords thy_name 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
+        else Export.export thy \<^path_binding>\<open>document/latex\<close> latex
       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);
 
 val defined_theory = is_some o lookup_theory;
 
 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 -> presentation_context option,
     commit: unit -> unit};
 
 fun theory_result theory =
   Result
    {theory = theory,
     exec_id = Document_ID.none,
     present = K NONE,
     commit = I};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_commit (Result {commit, ...}) = commit;
 
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;
 
 local
 
 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;
 
 fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
   | present_theory (Exn.Res (Result {theory, present, ...})) =
       (case present () of
         NONE => []
       | SOME (context as {segments, ...}) =>
           [Exn.capture (fn () => (apply_presentation context theory; (theory, segments))) ()]);
 
 in
 
 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 present_results = futures |> maps (present_theory o Future.join_result);
     val results2 = (map o Exn.map_res) (K ()) present_results;
 
     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 ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in Par_Exn.release_all present_results end);
 
 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.make_state NONE, 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 () : presentation_context =
       let
         val segments =
           (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) =>
             {span = span, prev_state = st, command = tr, state = st'});
       in {options = options, file_pos = text_pos, adjust_pos = I, segments = segments} 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 o 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 =
   ignore (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.make_state NONE);
   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,494 +1,494 @@
 /*  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.make_directory(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)",
         args => args.write(Path.explode(Export.MARKUP), args.snapshot.xml_markup())),
       Aspect("messages", "output messages (YXML format)",
         args => args.write(Path.explode(Export.MESSAGES), args.snapshot.messages.map(_._1))),
       Aspect("latex", "generated LaTeX source",
         args =>
           for {
             entry <- args.snapshot.exports
             if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
           } args.write(Path.explode(entry.name), entry.uncompressed)),
       Aspect("theory", "foundational theory content",
         args =>
           for {
             entry <- args.snapshot.exports
             if entry.name_has_prefix(Export.THEORY_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"
+            "pide_presentation" +
+            "editor_tracing_messages=0"
         aspects.foldLeft(options1) { case (opts, aspect) => aspect.options.foldLeft(opts)(_ + _) }
       }
 
       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): Unit = {
       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]): Unit = {
       errors.change(errs => errs ::: more_errs)
     }
 
     def check_errors: Unit = {
       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): Unit = {
       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 ((elem, pos) <- snapshot.messages if Protocol.is_error(elem))
                   yield {
                     "Error" + Position.here(pos) + ":\n" +
                       XML.content(Pretty.formatted(List(elem)))
                   }
                 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
   ): Unit = {
     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", Scala_Project.here,
       { 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.indent_lines(4, 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")
       })
 }