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,223 +1,222 @@
 (*: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
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -V           verbose latex
     -d DIR       include session directory
-    -n           no build of session
     -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, but
-  option \<^verbatim>\<open>-n\<close> suppresses that. 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).
+  @{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>-P\<close>, \<^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.
 
   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/Thy/present.scala b/src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala
+++ b/src/Pure/Thy/present.scala
@@ -1,493 +1,488 @@
 /*  Title:      Pure/Thy/present.scala
     Author:     Makarius
 
 Theory presentation: HTML and LaTeX documents.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 
 
 object Present
 {
   /* document variants */
 
   object Document_Variant
   {
     def parse(s: String): Document_Variant =
       Library.space_explode('=', s) match {
         case List(name) => Document_Variant(name)
         case List(name, tags) => Document_Variant(name, Library.space_explode(',', tags))
         case _ => error("Malformed document variant: " + quote(s))
       }
   }
 
   sealed case class Document_Variant(name: String, tags: List[String] = Nil)
   {
     def print: String = if (tags.isEmpty) name else name + "=" + tags.mkString(",")
     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 + "}"
           }))
   }
 
 
   /* 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.basic(info.chapter) + Path.basic(info.name)
   }
 
 
   /* 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 theory_link(name: Document.Node.Name): XML.Tree =
     HTML.link(html_name(name), HTML.text(name.theory_base_name))
 
   def session_html(
     session: String,
     deps: Sessions.Deps,
     store: Sessions.Store,
     presentation: Context): Path =
   {
     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 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 =
         for (doc <- info.documents)
           yield 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
     }
 
     val theories =
       using(Export.open_database_context(deps.sessions_structure, store))(context =>
         for {
           name <- base.session_theories
           entry <- context.try_entry(session, name.theory, document_html_name(name))
         } yield name -> entry.uncompressed(cache = store.xz_cache))
 
     val theories_body =
       HTML.itemize(for ((name, _) <- theories) yield List(theory_link(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"), theories_body)))))
 
     for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html)
 
     session_dir
   }
 
 
   /** 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,
     presentation: Context = Context.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_dir(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)
       Bytes.write(doc_dir + session_graph_path, graph_pdf)
 
       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)
     }
 
 
     /* produce documents */
 
     val doc_output = info.document_output
 
     val documents =
       for (doc <- info.documents)
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
           val (doc_dir, root) = prepare_dir(tmp_dir, doc)
           doc_output.foreach(prepare_dir(_, doc))
 
 
           // 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 doc -> Bytes.read(result_path)
         })
       }
 
     def output(dir: Path)
     {
       Isabelle_System.make_directory(dir)
       for ((doc, pdf) <- documents) {
         val path = dir + doc.path.pdf
         Bytes.write(path, pdf)
         progress.echo_document(path)
       }
     }
 
     if (presentation.enabled(info) || doc_output.isEmpty) {
       output(presentation.dir(store, info))
     }
 
     doc_output.foreach(output)
 
     documents
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("document", "prepare session theory document", args =>
     {
       var presentation = Present.Context.none
       var verbose_latex = false
       var dirs: List[Path] = Nil
-      var no_build = false
       var options = Options.init()
       var verbose_build = false
 
       val getopts = Getopts(
         """
 Usage: isabelle document [OPTIONS] SESSION
 
   Options are:
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -O           set option "document_output", relative to current directory
     -V           verbose latex
     -d DIR       include session directory
-    -n           no build of session
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose build
 
   Prepare the theory document of a session.
 """,
         "P:" -> (arg => presentation = Context.make(arg)),
         "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
         "V" -> (_ => verbose_latex = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
-        "n" -> (_ => no_build = true),
         "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 {
-        if (!no_build) {
-          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 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))
 
         build_documents(session, deps, store, progress = progress,
           presentation = presentation, verbose = true, verbose_latex = verbose_latex)
       }
     })
 }