diff --git a/etc/options b/etc/options
--- a/etc/options
+++ b/etc/options
@@ -1,360 +1,358 @@
 (* :mode=isabelle-options: *)
 
 section "Document Preparation"
 
 option browser_info : bool = false
   -- "generate theory browser information"
 
 option document : string = ""
   -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
   -- "document output directory"
-option document_output_sources : bool = true
-  -- "copy generated sources into document output directory"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
   -- "control line breaks in non-display material"
 option thy_output_cartouche : bool = false
   -- "indicate if the output should be delimited as cartouche"
 option thy_output_quotes : bool = false
   -- "indicate if the output should be delimited via double quotes"
 option thy_output_margin : int = 76
   -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
 option thy_output_source_cartouche : bool = false
   -- "print original source text rather than internal representation, preserve cartouches"
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
 
 section "Prover Output"
 
 option show_types : bool = false
   -- "show type constraints when printing terms"
 option show_sorts : bool = false
   -- "show sort constraints when printing types"
 option show_brackets : bool = false
   -- "show extra brackets when printing terms/types"
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"
 option goals_limit : int = 10
   -- "maximum number of subgoals to be printed"
 
 option names_long : bool = false
   -- "show fully qualified names"
 option names_short : bool = false
   -- "show base names only"
 option names_unique : bool = true
   -- "show partially qualified names, as required for unique name resolution"
 
 option eta_contract : bool = true
   -- "print terms in eta-contracted form"
 
 option print_mode : string = ""
   -- "additional print modes for prover output (separated by commas)"
 
 
 section "Parallel Processing"
 
 public option threads : int = 0
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
 option threads_stack_limit : real = 0.25
   -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 
 public option parallel_limit : int = 0
   -- "approximative limit for parallel tasks (0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 1
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_subproofs_threshold : real = 0.01
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
 option command_timing_threshold : real = 0.1
   -- "default threshold for persistent command timing (seconds)"
 
 
 section "Detail of Proof Checking"
 
 option record_proofs : int = -1
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
   -- "skip over proofs (implicit 'sorry')"
 option strict_facts : bool = false
   -- "force lazy facts when defined in context"
 
 
 section "Global Session Parameters"
 
 option condition : string = ""
   -- "required environment variables for subsequent theories (separated by commas)"
 
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
 option timeout_scale : real = 1.0
   -- "scale factor for session timeout"
 
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"
 
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
 option system_heaps : bool = false
   -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS"
 
 
 section "ML System"
 
 option ML_print_depth : int = 20
   -- "ML print depth for toplevel pretty-printing"
 
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
 public option ML_exception_debugger : bool = false
   -- "ML debugger exception trace for toplevel command execution"
 
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_system_64 : bool = false
   -- "ML system for 64bit platform is used if possible (change requires restart)"
 
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
 
 
 section "PIDE Build"
 
 option pide_reports : bool = true
   -- "report PIDE markup"
 
 
 section "Editor Session"
 
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
 public option editor_input_delay : real = 0.3
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0
   -- "delay for machine-generated input that may outperform user edits"
 
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
 public option editor_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
   -- "delay to prune history (delete old versions)"
 
 option editor_prune_size : int = 0
   -- "retained size of pruned history (delete old versions)"
 
 public option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
 public option editor_reparse_limit : int = 10000
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
   -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"
 
 public option editor_continuous_checking : bool = true
   -- "continuous checking of proof document (visible and required parts)"
 
 public option editor_output_state : bool = false
   -- "implicit output of proof state"
 
 option editor_execution_delay : real = 0.02
   -- "delay for start of execution process after document update (seconds)"
 
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
 public option editor_presentation : bool = false
   -- "dynamic presentation while editing"
 
 
 section "Headless Session"
 
 option headless_consolidate_delay : real = 15
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 option headless_prune_delay : real = 60
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5
   -- "delay for theory status check during PIDE processing (seconds)"
 
 option headless_check_limit : int = 0
   -- "maximum number of theory status checks (0 = unlimited)"
 
 option headless_nodes_status_delay : real = -1
   -- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)"
 
 option headless_watchdog_timeout : real = 600
   -- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)"
 
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
 option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
 section "Miscellaneous Tools"
 
 public option find_theorems_limit : int = 40
   -- "limit of displayed results"
 
 public option find_theorems_tactic_limit : int = 5
   -- "limit of tactic search for 'solves' criterion"
 
 
 section "Completion"
 
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
 public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
   -- "glob patterns to ignore in file-system path completion (separated by colons)"
 
 
 section "Spell Checker"
 
 public option spell_checker : bool = true
   -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_dictionary : string = "en"
   -- "spell-checker dictionary name"
 
 public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
 public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
 section "Secure Shell"
 
 option ssh_config_dir : string = "$HOME/.ssh"
   -- "SSH configuration directory"
 
 option ssh_config_file : string = "$HOME/.ssh/config"
   -- "main SSH configuration file"
 
 option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa"
   -- "possible SSH identity files (separated by colons)"
 
 option ssh_compression : bool = true
   -- "enable SSH compression"
 
 option ssh_connect_timeout : real = 60
   -- "SSH connection timeout (seconds)"
 
 option ssh_alive_interval : real = 30
   -- "time interval to keep SSH server connection alive (seconds)"
 
 option ssh_alive_count_max : int = 3
   -- "maximum number of messages to keep SSH server connection alive"
 
 
 section "Phabricator"
 
 option phabricator_version_arcanist : string = "68dba1a2c6d9fe1de7b9d4c944336458d0f016b3"
   -- "repository version for arcanist"
 
 option phabricator_version_phabricator : string = "5e06d924f8eba5df354c690ceb693e454e965d16"
   -- "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 = ""
diff --git a/src/Doc/System/Presentation.thy b/src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy
+++ b/src/Doc/System/Presentation.thy
@@ -1,221 +1,223 @@
 (*:maxLineLen=78:*)
 
 theory Presentation
 imports Base
 begin
 
 chapter \<open>Presenting theories \label{ch:present}\<close>
 
 text \<open>
   Isabelle provides several ways to present the outcome of formal
   developments, including WWW-based browsable libraries or actual printable
   documents. Presentation is centered around the concept of \<^emph>\<open>sessions\<close>
   (\chref{ch:session}). The global session structure is that of a tree, with
   Isabelle Pure at its root, further object-logics derived (e.g.\ HOLCF from
   HOL, and HOL from Pure), and application sessions further on in the
   hierarchy.
 
   The command-line tools @{tool_ref mkroot} and @{tool_ref build} provide the
   primary means for managing Isabelle sessions, including options for
   presentation: ``\<^verbatim>\<open>document=pdf\<close>'' generates PDF output from the theory
   session, and ``\<^verbatim>\<open>document_output=dir\<close>'' emits a copy of the document sources
   with the PDF into the given directory (relative to the session directory).
 
   Alternatively, @{tool_ref document} may be used to turn the generated
   {\LaTeX} sources of a session (exports from its build database) into PDF,
   using suitable invocations of @{tool_ref latex}.
 \<close>
 
 
 section \<open>Generating HTML browser information \label{sec:info}\<close>
 
 text \<open>
   As a side-effect of building sessions, Isabelle is able to generate theory
   browsing information, including HTML documents that show the theory sources
   and the relationship with its ancestors and descendants. Besides the HTML
   file that is generated for every theory, Isabelle stores links to all
   theories of a session in an index file. As a second hierarchy, groups of
   sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the
   implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
   for the presentation.
 
   \<^medskip>
   To generate theory browsing information for an existing session, just invoke
   @{tool build} with suitable options:
   @{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}
 
   The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
   reported by the above verbose invocation of the build process.
 
   Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
   \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are
   prepared automatically as well if enabled like this:
   @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
 
   Enabling both browser info and document preparation simultaneously causes an
   appropriate ``document'' link to be included in the HTML index. Documents
   may be generated independently of browser information as well, see
   \secref{sec:tool-document} for further details.
 
   \<^bigskip>
   The theory browsing information is stored in a sub-directory directory
   determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix
   corresponding to the session chapter and identifier. In order to present
   Isabelle applications on the web, the corresponding subdirectory from
   @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.
 \<close>
 
 
 section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
 
 text \<open>
   The @{tool_def mkroot} tool configures a given directory as session root,
   with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
 
   Options are:
     -A LATEX     provide author in LaTeX notation (default: user name)
     -I           init Mercurial repository and add generated files
     -T LATEX     provide title in LaTeX notation (default: session name)
     -n NAME      alternative session name (default: directory base name)
 
   Prepare session root directory (default: current directory).
 \<close>}
 
   The results are placed in the given directory \<open>dir\<close>, which refers to the
   current directory by default. The @{tool mkroot} tool is conservative in the
   sense that it does not overwrite existing files or directories. Earlier
   attempts to generate a session root need to be deleted manually.
 
   The generated session template will be accompanied by a formal document,
   with \<open>DIRECTORY\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see also
   \chref{ch:present}).
 
   Options \<^verbatim>\<open>-T\<close> and \<^verbatim>\<open>-A\<close> specify the document title and author explicitly,
   using {\LaTeX} source notation.
 
   Option \<^verbatim>\<open>-I\<close> initializes a Mercurial repository in the target directory, and
   adds all generated files (without commit).
 
   Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
   of the given directory is used.
 
   \<^medskip>
   The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
   the parent session.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:
   @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}
 
   \<^medskip>
   Upgrade the current directory into a session ROOT with document preparation,
   and build it:
   @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}
 \<close>
 
 
 section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
 
 text \<open>
   The @{tool_def document} tool prepares logic session documents. Its usage
   is:
   @{verbatim [display]
 \<open>Usage: isabelle document [OPTIONS] SESSION
 
   Options are:
-    -O           set option "document_output", relative to current directory
+    -O DIR       output directory for LaTeX sources and resulting PDF
+    -P DIR       output directory for resulting PDF
+    -S DIR       output directory for LaTeX sources
     -V           verbose latex
     -d DIR       include session directory
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose build
 
   Prepare the theory document of a session.\<close>}
 
   Generated {\LaTeX} sources are taken from the session build database:
   @{tool_ref build} is invoked beforehand to ensure that it is up-to-date.
   Further files are generated on the spot, notably essential Isabelle style
   files, and \<^verbatim>\<open>session.tex\<close> to input all theory sources from the session
   (excluding imports from other sessions).
 
   \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool
   build}.
 
   \<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.
 
-  \<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the @{system_option document_output} option
-  relative to the current directory, while \<^verbatim>\<open>-o document_output=\<close>\<open>dir\<close> is
-  relative to the session directory.
+  \<^medskip> Option \<^verbatim>\<open>-O\<close>~\<open>dir\<close> specifies the output directory for generated {\LaTeX}
+  sources and the result PDF file. Options \<^verbatim>\<open>-P\<close> and \<^verbatim>\<open>-S\<close> only refer to the
+  PDF and sources, respectively.
 
   For example, for output directory ``\<^verbatim>\<open>output\<close>'' and the default document
   variant ``\<^verbatim>\<open>document\<close>'', the generated document sources are placed into the
   subdirectory \<^verbatim>\<open>output/document/\<close> and the resulting PDF into
   \<^verbatim>\<open>output/document.pdf\<close>.
 
   \<^medskip> Isabelle is usually smart enough to create the PDF from the given
   \<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index)
   using standard {\LaTeX} tools. Alternatively, \isakeyword{document\_files}
   in the session \<^verbatim>\<open>ROOT\<close> may include an executable \<^verbatim>\<open>build\<close> script to take
   care of that. It is invoked with command-line arguments for the document
   format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs to produce
   corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default document variants
   (the main work can be delegated to @{tool latex}). \<close>
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Produce the document from session \<^verbatim>\<open>FOL\<close> with full verbosity, and a copy in
   the current directory (subdirectory \<^verbatim>\<open>document\<close> and file \<^verbatim>\<open>document.pdf)\<close>:
 
   @{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>}
 \<close>
 
 
 section \<open>Running {\LaTeX} within the Isabelle environment
   \label{sec:tool-latex}\<close>
 
 text \<open>
   The @{tool_def latex} tool provides the basic interface for Isabelle
   document preparation. Its usage is:
   @{verbatim [display]
 \<open>Usage: isabelle latex [OPTIONS] [FILE]
 
   Options are:
     -o FORMAT    specify output format: pdf (default), bbl, idx, sty
 
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.\<close>}
 
   Appropriate {\LaTeX}-related programs are run on the input file, according
   to the given output format: @{executable pdflatex}, @{executable bibtex}
   (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands
   are determined from the settings environment (@{setting ISABELLE_PDFLATEX}
   etc.).
 
   The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
   the distribution. This is useful in special situations where the document
   sources are to be processed another time by separate tools.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Invoking @{tool latex} by hand may be occasionally useful when debugging
   failed attempts of the automatic document preparation stage of batch-mode
   Isabelle. The abortive process leaves the sources at a certain place within
   @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
   This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
   this:
 
   @{verbatim [display]
 \<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
 isabelle latex -o pdf\<close>}
 \<close>
 
 end
diff --git a/src/Pure/Admin/build_doc.scala b/src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala
+++ b/src/Pure/Admin/build_doc.scala
@@ -1,101 +1,105 @@
 /*  Title:      Pure/Admin/build_doc.scala
     Author:     Makarius
 
 Build Isabelle documentation.
 */
 
 package isabelle
 
 
 object Build_Doc
 {
   /* build_doc */
 
   def build_doc(
     options: Options,
     progress: Progress = new Progress,
     all_docs: Boolean = false,
     max_jobs: Int = 1,
     docs: List[String] = Nil)
   {
     val store = Sessions.store(options)
 
     val sessions_structure = Sessions.load_structure(options)
     val selected =
       for {
         session <- sessions_structure.build_topological_order
         info = sessions_structure(session)
         if info.groups.contains("doc")
         doc = info.options.string("document_variants")
         if all_docs || docs.contains(doc)
       } yield (doc, session)
 
     val documents = selected.map(_._1)
     val selection = Sessions.Selection(sessions = selected.map(_._2))
 
     docs.filter(doc => !documents.contains(doc)) match {
       case Nil =>
       case bad => error("No documentation session for " + commas_quote(bad))
     }
 
     progress.echo("Build started for sessions " + commas_quote(selection.sessions))
     Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).ok ||
       error("Build failed")
 
     progress.echo("Build started for documentation " + commas_quote(documents))
-    val doc_options =
-      options + "document=pdf" + "document_output=~~/doc" + "document_output_sources=false"
+    val doc_options = options + "document=pdf"
     val deps = Sessions.load_structure(doc_options).selection_deps(selection)
 
     val errs =
-      Par_List.map((doc_session: (String, String)) =>
-        try {
-          Presentation.build_documents(doc_session._2, deps, store, progress = progress)
-          None
-        }
-        catch {
-          case Exn.Interrupt.ERROR(msg) =>
-            val sep = if (msg.contains('\n')) "\n" else " "
-            Some("Documentation " + doc_session._1 + " failed:" + sep + msg)
-        }, selected).flatten
+      Par_List.map[(String, String), Option[String]](
+      {
+        case (doc, session) =>
+          try {
+            progress.echo("Documentation " + doc + " ...")
+            Presentation.build_documents(session, deps, store,
+              output_pdf = Some(Path.explode("~~/src/doc")))
+            None
+          }
+          catch {
+            case Exn.Interrupt.ERROR(msg) =>
+              val sep = if (msg.contains('\n')) "\n" else " "
+              Some("Documentation " + doc + " failed:" + sep + msg)
+          }
+      }, selected).flatten
 
     if (errs.nonEmpty) error(cat_lines(errs))
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
     {
       var all_docs = false
       var max_jobs = 1
       var options = Options.init()
 
       val getopts =
         Getopts("""
 Usage: isabelle build_doc [OPTIONS] [DOCS ...]
 
   Options are:
     -a           select all documentation sessions
     -j INT       maximum number of parallel jobs (default 1)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
 
   Build Isabelle documentation from documentation sessions with
   suitable document_variants entry.
 """,
           "a" -> (_ => all_docs = true),
           "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
           "o:" -> (arg => options = options + arg))
 
       val docs = getopts(args)
 
       if (!all_docs && docs.isEmpty) getopts.usage()
 
       val progress = new Console_Progress()
 
       progress.interrupt_handler {
         build_doc(options, progress, all_docs, max_jobs, docs)
       }
     })
 }
diff --git a/src/Pure/Thy/presentation.scala b/src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala
+++ b/src/Pure/Thy/presentation.scala
@@ -1,653 +1,668 @@
 /*  Title:      Pure/Thy/present.scala
     Author:     Makarius
 
 Theory presentation: HTML and LaTeX documents.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 
 
 object Presentation
 {
   /* document variants */
 
   object Document_Variant
   {
     def parse(name: String, tags: String): Document_Variant =
       Document_Variant(name, Library.space_explode(',', tags))
 
     def parse(opt: String): Document_Variant =
       Library.space_explode('=', opt) match {
         case List(name) => Document_Variant(name, Nil)
         case List(name, tags) => parse(name, tags)
         case _ => error("Malformed document variant: " + quote(opt))
       }
   }
 
   sealed case class Document_Variant(name: String, tags: List[String], sources: String = "")
   {
     def print_tags: String = tags.mkString(",")
     def print: String = if (tags.isEmpty) name else name + "=" + print_tags
 
     def path: Path = Path.basic(name)
 
     def latex_sty: String =
       Library.terminate_lines(
         tags.map(tag =>
           tag.toList match {
             case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
             case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
             case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
             case cs => "\\isakeeptag{" + cs.mkString + "}"
           }))
 
     def set_sources(s: String): Document_Variant = copy(sources = s)
   }
 
 
   /* SQL data model */
 
   object Data
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
     val tags = SQL.Column.string("tags")
     val sources = SQL.Column.string("sources")
     val pdf = SQL.Column.bytes("pdf")
 
     val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
       "WHERE " + Data.session_name.equal(session_name) +
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
   def read_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] =
   {
     val select =
       Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
       {
         val name = res.string(Data.name)
         val tags = res.string(Data.tags)
         val sources = res.string(Data.sources)
         Document_Variant.parse(name, tags).set_sources(sources)
       }).toList)
   }
 
   def read_document(db: SQL.Database, session_name: String, name: String)
     : Option[(Document_Variant, Bytes)] =
   {
     val select = Data.table.select(sql = Data.where_equal(session_name, name))
     db.using_statement(select)(stmt =>
     {
       val res = stmt.execute_query()
       if (res.next()) {
         val name = res.string(Data.name)
         val tags = res.string(Data.tags)
         val sources = res.string(Data.sources)
         val pdf = res.bytes(Data.pdf)
         Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf)
       }
       else None
     })
   }
 
   def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes)
   {
     db.using_statement(Data.table.insert())(stmt =>
     {
       stmt.string(1) = session_name
       stmt.string(2) = doc.name
       stmt.string(3) = doc.print_tags
       stmt.string(4) = doc.sources
       stmt.bytes(5) = pdf
       stmt.execute()
     })
   }
 
 
   /* presentation context */
 
   object Context
   {
     val none: Context = new Context { def enabled: Boolean = false }
     val standard: Context = new Context { def enabled: Boolean = true }
 
     def dir(path: Path): Context =
       new Context {
         def enabled: Boolean = true
         override def dir(store: Sessions.Store): Path = path
       }
 
     def make(s: String): Context =
       if (s == ":") standard else dir(Path.explode(s))
   }
 
   abstract class Context private
   {
     def enabled: Boolean
     def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
     def dir(store: Sessions.Store): Path = store.presentation_dir
     def dir(store: Sessions.Store, info: Sessions.Info): Path =
       dir(store) + Path.explode(info.chapter_session)
   }
 
 
   /* maintain chapter index -- NOT thread-safe */
 
   private val sessions_path = Path.basic(".sessions")
 
   private def read_sessions(dir: Path): List[(String, String)] =
   {
     val path = dir + sessions_path
     if (path.is_file) {
       import XML.Decode._
       list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
     }
     else Nil
   }
 
   private def write_sessions(dir: Path, sessions: List[(String, String)])
   {
     import XML.Encode._
     File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
   }
 
   def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
   {
     val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter))
 
     val sessions0 =
       try { read_sessions(dir) }
       catch { case _: XML.Error => Nil }
 
     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
     write_sessions(dir, sessions)
 
     val title = "Isabelle/" + chapter + " sessions"
     HTML.write_document(dir, "index.html",
       List(HTML.title(title + " (" + Distribution.version + ")")),
       HTML.chapter(title) ::
        (if (sessions.isEmpty) Nil
         else
           List(HTML.div("sessions",
             List(HTML.description(
               sessions.map({ case (name, description) =>
                 val descr = Symbol.trim_blank_lines(description)
                 (List(HTML.link(name + "/index.html", HTML.text(name))),
                   if (descr == "") Nil
                   else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))))
   }
 
   def make_global_index(browser_info: Path)
   {
     if (!(browser_info + Path.explode("index.html")).is_file) {
       Isabelle_System.make_directory(browser_info)
       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
         browser_info + Path.explode("isabelle.gif"))
       File.write(browser_info + Path.explode("index.html"),
         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
         File.read(Path.explode("~~/lib/html/library_index_content.template")) +
         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
     }
   }
 
 
   /* present session */
 
   val session_graph_path = Path.explode("session_graph.pdf")
   val readme_path = Path.basic("README.html")
 
   def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
   def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name)
 
   def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = {
     if (keywords.is_command(tok, Keyword.theory_end))
       List(Markup.KEYWORD2, Markup.KEYWORD)
     else if (keywords.is_command(tok, Keyword.proof_asm))
       List(Markup.KEYWORD3, Markup.COMMAND)
     else if (keywords.is_command(tok, Keyword.improper))
       List(Markup.KEYWORD1, Markup.IMPROPER, Markup.COMMAND)
     else if (tok.is_command) List(Markup.KEYWORD1, Markup.COMMAND)
     else if (tok.is_delimiter) List(Markup.DELIMITER, Markup.KEYWORD)
     else if (tok.is_keyword) List(Markup.KEYWORD2, Markup.KEYWORD)
     else if (tok.is_comment) List(Markup.COMMENT)
     else {
       tok.kind match {
         case Token.Kind.VAR => List(Markup.VAR)
         case Token.Kind.TYPE_IDENT => List(Markup.TFREE)
         case Token.Kind.TYPE_VAR => List(Markup.TVAR)
         case Token.Kind.STRING => List(Markup.STRING)
         case Token.Kind.ALT_STRING => List(Markup.ALT_STRING)
         case Token.Kind.VERBATIM => List(Markup.VERBATIM)
         case Token.Kind.CARTOUCHE => List(Markup.CARTOUCHE)
         case _ => Nil
       }
     }
   }
 
   def session_html(
     session: String,
     deps: Sessions.Deps,
     store: Sessions.Store,
     presentation: Context) =
   {
     val info = deps.sessions_structure(session)
     val options = info.options
     val base = deps(session)
 
     val session_dir = presentation.dir(store, info)
     val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
     for (entry <- Isabelle_Fonts.fonts(hidden = true))
       File.copy(entry.path, session_fonts)
 
     Bytes.write(session_dir + session_graph_path,
       graphview.Graph_File.make_pdf(options, base.session_graph_display))
 
     val documents =
       using(store.open_database(session))(db =>
         for {
           doc <- info.document_variants
           (_, pdf) <- Presentation.read_document(db, session, doc.name)
         } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc })
 
     val links =
     {
       val deps_link =
         HTML.link(session_graph_path, HTML.text("theory dependencies"))
 
       val readme_links =
         if ((info.dir + readme_path).is_file) {
           File.copy(info.dir + readme_path, session_dir + readme_path)
           List(HTML.link(readme_path, HTML.text("README")))
         }
         else Nil
 
       val document_links =
         documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name)))
 
       Library.separate(HTML.break ::: HTML.nl,
         (deps_link :: readme_links ::: document_links).
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
     def theory_link(name1: Document.Node.Name, body: XML.Body): XML.Tree =
     {
       val session1 = base.theory_qualifier(name1)
       val info1 = deps.sessions_structure(session1)
       val prefix =
         if (session == session1) ""
         else if (info.chapter == info1.chapter) "../" + session1 + "/"
         else "../../" + info1.chapter_session + "/"
       HTML.link(prefix + html_name(name1), body)
     }
 
     val theories =
       for (name <- base.session_theories)
       yield {
         val syntax = base.theory_syntax(name)
         val keywords = syntax.keywords
         val spans = syntax.parse_spans(Symbol.decode(File.read(name.path)))
 
         val thy_body =
         {
           val imports_offset = base.known_theories(name.theory).header.imports_offset
           var token_offset = 1
           spans.flatMap(span =>
           {
             val is_init = span.is_kind(keywords, Keyword.theory_begin, false)
             span.content.flatMap(tok =>
             {
               val text = HTML.text(tok.source)
               val item =
                 if (is_init && imports_offset.isDefinedAt(token_offset)) {
                   List(theory_link(imports_offset(token_offset), text))
                 }
                 else text
 
               token_offset += tok.symbol_length
 
               (token_markups(keywords, tok) :\ item)(
                 { case (c, body) => List(HTML.span(c, body)) })
             })
           })
         }
 
         val title = "Theory " + name.theory_base_name
         HTML.write_document(session_dir, html_name(name),
           List(HTML.title(title)),
           HTML.div("head", List(HTML.chapter(title))) :: List(HTML.pre("source", thy_body)))
 
         List(HTML.link(html_name(name), HTML.text(name.theory_base_name)))
       }
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
       List(HTML.title(title + " (" + Distribution.version + ")")),
       HTML.div("head", List(HTML.chapter(title), HTML.par(links))) ::
        (if (theories.isEmpty) Nil
         else List(HTML.div("theories", List(HTML.section("Theories"), HTML.itemize(theories))))))
   }
 
 
   /** preview **/
 
   sealed case class Preview(title: String, content: String)
 
   def preview(
     resources: Resources,
     snapshot: Document.Snapshot,
     plain_text: Boolean = false,
     fonts_url: String => String = HTML.fonts_url()): Preview =
   {
     require(!snapshot.is_outdated)
 
     def output_document(title: String, body: XML.Body): String =
       HTML.output_document(
         List(
           HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
           HTML.title(title)),
         List(HTML.source(body)), css = "", structural = false)
 
     val name = snapshot.node_name
 
     if (plain_text) {
       val title = "File " + quote(name.path.file_name)
       val content = output_document(title, HTML.text(snapshot.node.source))
       Preview(title, content)
     }
     else {
       resources.make_preview(snapshot) match {
         case Some(preview) => preview
         case None =>
           val title =
             if (name.is_theory) "Theory " + quote(name.theory_base_name)
             else "File " + quote(name.path.file_name)
           val content = output_document(title, pide_document(snapshot))
           Preview(title, content)
       }
     }
   }
 
 
   /* PIDE document */
 
   private val document_elements =
     Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
     Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
 
   private val div_elements =
     Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
       HTML.descr.name)
 
   private def html_div(html: XML.Body): Boolean =
     html exists {
       case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
       case XML.Text(_) => false
     }
 
   private def html_class(c: String, html: XML.Body): XML.Tree =
     if (html.forall(_ == HTML.no_text)) HTML.no_text
     else if (html_div(html)) HTML.div(c, html)
     else HTML.span(c, html)
 
   private def make_html(xml: XML.Body): XML.Body =
     xml map {
       case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
         html_class(Markup.Language.DOCUMENT, make_html(body))
       case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
       case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
       case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
       case XML.Elem(Markup.Markdown_List(kind), body) =>
         if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
       case XML.Elem(markup, body) =>
         val name = markup.name
         val html =
           markup.properties match {
             case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
               List(html_class(kind, make_html(body)))
             case _ =>
               make_html(body)
           }
         Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
           case Some(c) => html_class(c.toString, html)
           case None => html_class(name, html)
         }
       case XML.Text(text) =>
         XML.Text(Symbol.decode(text))
     }
 
   def pide_document(snapshot: Document.Snapshot): XML.Body =
     make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
 
 
 
   /** build documents **/
 
   val session_tex_path = Path.explode("session.tex")
 
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
   def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
 
   def build_documents(
     session: String,
     deps: Sessions.Deps,
     store: Sessions.Store,
     progress: Progress = new Progress,
+    output_sources: Option[Path] = None,
+    output_pdf: Option[Path] = None,
     verbose: Boolean = false,
     verbose_latex: Boolean = false): List[(Document_Variant, Bytes)] =
   {
     /* session info */
 
     val info = deps.sessions_structure(session)
     val options = info.options
     val base = deps(session)
     val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
 
 
     /* prepare document directory */
 
     lazy val tex_files =
       using(Export.open_database_context(deps.sessions_structure, store))(context =>
         for (name <- base.session_theories ::: base.document_theories)
         yield {
           val entry = context.entry(session, name.theory, document_tex_name(name))
           Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
         }
       )
 
     def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) =
     {
       val doc_dir = dir + Path.basic(doc.name)
       Isabelle_System.make_directory(doc_dir)
 
       Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
       File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty)
       for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir)
 
       File.write(doc_dir + session_tex_path,
         Library.terminate_lines(
           base.session_theories.map(name => "\\input{" + tex_name(name) + "}")))
 
       for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex)
 
       val root1 = "root_" + doc.name
       val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root"
 
       (doc_dir, root)
     }
 
     def prepare_dir2(dir: Path, doc: Document_Variant): Unit =
     {
       val doc_dir = dir + Path.basic(doc.name)
 
       // non-deterministic, but irrelevant
       Bytes.write(doc_dir + session_graph_path, graph_pdf)
     }
 
 
     /* produce documents */
 
-    val doc_output = info.document_output
-
     val documents =
       for (doc <- info.documents)
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
           progress.echo_document("Building document " + session + "/" + doc.name + " ...")
           val start = Time.now()
 
 
           // prepare sources
 
           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
           val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
           val sources = SHA1.digest_set(digests).toString
           prepare_dir2(tmp_dir, doc)
 
-          doc_output.foreach(prepare_dir1(_, doc))
-          doc_output.foreach(prepare_dir2(_, doc))
+          for (dir <- output_sources) {
+            prepare_dir1(dir, doc)
+            prepare_dir2(dir, doc)
+          }
 
 
           // old document from database
 
           val old_document =
             using(store.open_database(session))(db =>
               for {
                 document@(doc, pdf) <- read_document(db, session, doc.name)
                 if doc.sources == sources
               }
               yield {
                 Bytes.write(doc_dir + doc.path.pdf, pdf)
                 document
               })
 
           old_document getOrElse {
             // bash scripts
 
             def root_bash(ext: String): String = Bash.string(root + "." + ext)
 
             def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
               "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
 
             def bash(items: String*): Process_Result =
               progress.bash(items.mkString(" && "), cwd = doc_dir.file,
                 echo = verbose_latex, watchdog = Time.seconds(0.5))
 
 
             // prepare document
 
             val result =
               if ((doc_dir + Path.explode("build")).is_file) {
                 bash("./build pdf " + Bash.string(doc.name))
               }
               else {
                 bash(
                   latex_bash(),
                   "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
                   "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
                   latex_bash(),
                   latex_bash())
               }
 
 
             // result
 
             val root_pdf = Path.basic(root).pdf
             val result_path = doc_dir + root_pdf
 
             if (!result.ok) {
               cat_error(
                 Library.trim_line(result.err),
                 cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
                 "Failed to build document " + quote(doc.name))
             }
             else if (!result_path.is_file) {
               error("Bad document result: expected to find " + root_pdf)
             }
             else {
               val stop = Time.now()
               val timing = stop - start
               progress.echo_document("Finished document " + session + "/" + doc.name +
                 " (" + timing.message_hms + " elapsed time)")
 
               doc.set_sources(sources) -> Bytes.read(result_path)
             }
           }
         })
       }
 
-    for (dir <- doc_output; (doc, pdf) <- documents) {
+    for (dir <- output_pdf; (doc, pdf) <- documents) {
+      Isabelle_System.make_directory(dir)
       val path = dir + doc.path.pdf
       Bytes.write(path, pdf)
       progress.echo_document("Document at " + path.absolute)
     }
 
     documents
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("document", "prepare session theory document", args =>
     {
+      var output_sources: Option[Path] = None
+      var output_pdf: Option[Path] = None
       var verbose_latex = false
       var dirs: List[Path] = Nil
       var options = Options.init()
       var verbose_build = false
 
       val getopts = Getopts(
         """
 Usage: isabelle document [OPTIONS] SESSION
 
   Options are:
-    -O           set option "document_output", relative to current directory
+    -O DIR       output directory for LaTeX sources and resulting PDF
+    -P DIR       output directory for resulting PDF
+    -S DIR       output directory for LaTeX sources
     -V           verbose latex
     -d DIR       include session directory
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose build
 
   Prepare the theory document of a session.
 """,
-        "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
+        "O:" -> (arg =>
+          {
+            val dir = Path.explode(arg)
+            output_sources = Some(dir)
+            output_pdf = Some(dir)
+          }),
+        "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }),
+        "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }),
         "V" -> (_ => verbose_latex = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "o:" -> (arg => options = options + arg),
         "v" -> (_ => verbose_build = true))
 
       val more_args = getopts(args)
       val session =
         more_args match {
           case List(a) => a
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress(verbose = verbose_build)
       val store = Sessions.store(options)
 
       progress.interrupt_handler {
         val res =
           Build.build(options, selection = Sessions.Selection.session(session),
             dirs = dirs, progress = progress, verbose = verbose_build)
         if (!res.ok) error("Failed to build session " + quote(session))
 
         val deps =
           Sessions.load_structure(options + "document=pdf", dirs = dirs).
             selection_deps(Sessions.Selection.session(session))
 
-        if (deps.sessions_structure(session).document_output.isEmpty) {
-          progress.echo_warning("No document_output")
+        if (output_sources.isEmpty && output_pdf.isEmpty) {
+          progress.echo_warning("No output directory")
         }
 
         build_documents(session, deps, store, progress = progress,
+          output_sources = output_sources, output_pdf = output_pdf,
           verbose = true, verbose_latex = verbose_latex)
       }
     })
 }
diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala
+++ b/src/Pure/Tools/build_job.scala
@@ -1,310 +1,315 @@
 /*  Title:      Pure/Tools/build_job.scala
     Author:     Makarius
 
 Build job running prover process, with rudimentary PIDE session.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 class Build_Job(progress: Progress,
   session_name: String,
   val info: Sessions.Info,
   deps: Sessions.Deps,
   store: Sessions.Store,
   do_store: Boolean,
   presentation: Presentation.Context,
   verbose: Boolean,
   val numa_node: Option[Int],
   command_timings0: List[Properties.T])
 {
   val options: Options = NUMA.policy_options(info.options, numa_node)
 
   private val sessions_structure = deps.sessions_structure
 
   private val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")
       val base = deps(parent)
 
       val env =
         Isabelle_System.settings() +
           ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
       val is_pure = Sessions.is_pure(session_name)
 
       val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
 
       val eval_store =
         if (do_store) {
           (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
           List("ML_Heap.save_child " +
             ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
         }
         else Nil
 
       val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
           override val xml_cache: XML.Cache = store.xml_cache
           override val xz_cache: XZ.Cache = store.xz_cache
         }
 
       object Build_Session_Errors
       {
         private val promise: Promise[List[String]] = Future.promise
 
         def result: Exn.Result[List[String]] = promise.join_result
         def cancel: Unit = promise.cancel
         def apply(errs: List[String])
         {
           try { promise.fulfill(errs) }
           catch { case _: IllegalStateException => }
         }
       }
 
       val export_consumer =
         Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
 
       val stdout = new StringBuilder(1000)
       val stderr = new StringBuilder(1000)
       val messages = new mutable.ListBuffer[XML.Elem]
       val command_timings = new mutable.ListBuffer[Properties.T]
       val theory_timings = new mutable.ListBuffer[Properties.T]
       val session_timings = new mutable.ListBuffer[Properties.T]
       val runtime_statistics = new mutable.ListBuffer[Properties.T]
       val task_statistics = new mutable.ListBuffer[Properties.T]
       val document_output = new mutable.ListBuffer[String]
 
       def fun(
         name: String,
         acc: mutable.ListBuffer[Properties.T],
         unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
       {
         name -> ((msg: Prover.Protocol_Output) =>
           unapply(msg.properties) match {
             case Some(props) => acc += props; true
             case _ => false
           })
       }
 
       session.init_protocol_handler(new Session.Protocol_Handler
         {
           override def exit() { Build_Session_Errors.cancel }
 
           private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
           {
             val (rc, errors) =
               try {
                 val (rc, errs) =
                 {
                   import XML.Decode._
                   pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                 }
                 val errors =
                   for (err <- errs) yield {
                     val prt = Protocol_Message.expose_no_reports(err)
                     Pretty.string_of(prt, metric = Symbol.Metric)
                   }
                 (rc, errors)
               }
               catch { case ERROR(err) => (2, List(err)) }
 
             session.protocol_command("Prover.stop", rc.toString)
             Build_Session_Errors(errors)
             true
           }
 
           private def loading_theory(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Markup.Loading_Theory(name) =>
                 progress.theory(Progress.Theory(name, session = session_name))
                 true
               case _ => false
             }
 
           private def export(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Protocol.Export(args) =>
                 export_consumer(session_name, args, msg.bytes)
                 true
               case _ => false
             }
 
           private def command_timing(props: Properties.T): Option[Properties.T] =
             for {
               props1 <- Markup.Command_Timing.unapply(props)
               elapsed <- Markup.Elapsed.unapply(props1)
               elapsed_time = Time.seconds(elapsed)
               if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
             } yield props1.filter(p => Markup.command_timing_properties(p._1))
 
           override val functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
               Markup.EXPORT -> export,
               fun(Markup.Command_Timing.name, command_timings, command_timing),
               fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
               fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
               fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
         })
 
       session.runtime_statistics += Session.Consumer("ML_statistics")
         {
           case Session.Runtime_Statistics(props) => runtime_statistics += props
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")
         {
           case msg: Prover.Output =>
             val message = msg.message
             if (msg.is_stdout) {
               stdout ++= Symbol.encode(XML.content(message))
             }
             else if (msg.is_stderr) {
               stderr ++= Symbol.encode(XML.content(message))
             }
             else if (Protocol.is_exported(message)) {
               messages += message
             }
             else if (msg.is_exit) {
               val err =
                 "Prover terminated" +
                   (msg.properties match {
                     case Markup.Process_Result(result) => ": " + result.print_rc
                     case _ => ""
                   })
               Build_Session_Errors(List(err))
             }
           case _ =>
         }
 
       val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
       val process =
         Isabelle_Process(session, options, sessions_structure, store,
           logic = parent, raw_ml_system = is_pure,
           use_prelude = use_prelude, eval_main = eval_main,
           cwd = info.dir.file, env = env)
 
       val build_errors =
         Isabelle_Thread.interrupt_handler(_ => process.terminate) {
           Exn.capture { process.await_startup } match {
             case Exn.Res(_) =>
               val resources_yxml = resources.init_session_yxml
               val args_yxml =
                 YXML.string_of_body(
                   {
                     import XML.Encode._
                     pair(string, list(pair(Options.encode, list(pair(string, properties)))))(
                       (session_name, info.theories))
                   })
               session.protocol_command("build_session", resources_yxml, args_yxml)
               Build_Session_Errors.result
             case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
           }
         }
 
       val process_result =
         Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
 
       val export_errors =
         export_consumer.shutdown(close = true).map(Output.error_message_text)
 
       val document_errors =
         try {
-          if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
+          if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
+          {
             val document_progress =
               new Progress {
                 override def echo(msg: String): Unit =
                   document_output.synchronized { document_output += msg }
                 override def echo_document(msg: String): Unit =
                   progress.echo_document(msg)
               }
             val documents =
-              Presentation.build_documents(session_name, deps, store, verbose = verbose,
-                verbose_latex = true, progress = document_progress)
+              Presentation.build_documents(session_name, deps, store,
+                output_sources = info.document_output,
+                output_pdf = info.document_output,
+                progress = document_progress,
+                verbose = verbose,
+                verbose_latex = true)
             using(store.open_database(session_name, output = true))(db =>
               for ((doc, pdf) <- documents) {
                 db.transaction {
                   Presentation.write_document(db, session_name, doc, pdf)
                 }
               })
           }
           Nil
         }
         catch { case Exn.Interrupt.ERROR(msg) => List(msg) }
 
       val result =
       {
         val more_output =
           Library.trim_line(stdout.toString) ::
             messages.toList.map(message =>
               Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
             document_output.toList
 
         val more_errors =
           Library.trim_line(stderr.toString) :: export_errors ::: document_errors
 
         process_result.output(more_output).errors(more_errors)
       }
 
       build_errors match {
         case Exn.Res(build_errs) =>
           val errs = build_errs ::: document_errors
           if (errs.isEmpty) result
           else {
             result.error_rc.output(
               errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                 errs.map(Protocol.Error_Message_Marker.apply))
           }
         case Exn.Exn(Exn.Interrupt()) =>
           if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
         case Exn.Exn(exn) => throw exn
       }
     }
 
   def terminate: Unit = future_result.cancel
   def is_finished: Boolean = future_result.is_finished
 
   private val timeout_request: Option[Event_Timer.Request] =
   {
     if (info.timeout > Time.zero)
       Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
     else None
   }
 
   def join: (Process_Result, Option[String]) =
   {
     val result1 = future_result.join
 
     val was_timeout =
       timeout_request match {
         case None => false
         case Some(request) => !request.cancel
       }
 
     val result2 =
       if (result1.interrupted) {
         if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
         else result1.error(Output.error_message_text("Interrupt"))
       }
       else result1
 
     val heap_digest =
       if (result2.ok && do_store && store.output_heap(session_name).is_file)
         Some(Sessions.write_heap_digest(store.output_heap(session_name)))
       else None
 
     (result2, heap_digest)
   }
 }