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,101 @@
 /*  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 deps = Sessions.load_structure(doc_options).selection_deps(selection)
 
     val errs =
       Par_List.map((doc_session: (String, String)) =>
         try {
-          Present.build_documents(doc_session._2, deps, store, progress = progress)
+          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
 
     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/PIDE/resources.scala b/src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala
+++ b/src/Pure/PIDE/resources.scala
@@ -1,448 +1,448 @@
 /*  Title:      Pure/PIDE/resources.scala
     Author:     Makarius
 
 Resources for theories and auxiliary files.
 */
 
 package isabelle
 
 
 import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}
 
 
 class Resources(
   val sessions_structure: Sessions.Structure,
   val session_base: Sessions.Base,
   val log: Logger = No_Logger,
   command_timings: List[Properties.T] = Nil)
 {
   resources =>
 
 
   /* init session */
 
   def init_session_yxml: String =
   {
     import XML.Encode._
 
     YXML.string_of_body(
       pair(list(pair(string, int)),
       pair(list(pair(string, properties)),
       pair(list(pair(string, string)),
       pair(list(pair(string, string)),
       pair(list(pair(string, list(string))),
       pair(list(properties),
       pair(list(string),
       pair(list(pair(string, string)), list(string)))))))))(
        (Symbol.codes,
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
        (sessions_structure.session_chapters,
        (sessions_structure.bibtex_entries,
        (command_timings,
        (session_base.doc_names,
        (session_base.global_theories.toList,
         session_base.loaded_theories.keys))))))))))
   }
 
 
   /* file formats */
 
   def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
     File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name))
 
   def make_theory_content(thy_name: Document.Node.Name): Option[String] =
     File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
 
-  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+  def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
     File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
 
   def is_hidden(name: Document.Node.Name): Boolean =
     !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
 
   def thy_path(path: Path): Path = path.ext("thy")
 
 
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
   def append(node_name: Document.Node.Name, source_path: Path): String =
     append(node_name.master_dir, source_path)
 
   def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name =
   {
     val node = append(dir, file)
     val master_dir = append(dir, file.dir)
     Document.Node.Name(node, master_dir, theory)
   }
 
   def loaded_theory_node(theory: String): Document.Node.Name =
     Document.Node.Name(theory, "", theory)
 
 
   /* source files of Isabelle/ML bootstrap */
 
   def source_file(raw_name: String): Option[String] =
   {
     if (Path.is_wellformed(raw_name)) {
       if (Path.is_valid(raw_name)) {
         def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
 
         val path = Path.explode(raw_name)
         val path1 =
           if (path.is_absolute || path.is_current) check(path)
           else {
             check(Path.explode("~~/src/Pure") + path) orElse
               (if (Isabelle_System.getenv("ML_SOURCES") == "") None
                else check(Path.explode("$ML_SOURCES") + path))
           }
         Some(File.platform_path(path1 getOrElse path))
       }
       else None
     }
     else Some(raw_name)
   }
 
 
   /* theory files */
 
   def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
   {
     val (is_utf8, raw_text) =
       with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
     () => {
       if (syntax.load_commands_in(raw_text)) {
         val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
         val spans = syntax.parse_spans(text)
         val dir = Path.explode(name.master_dir)
         spans.iterator.flatMap(Command.span_files(syntax, _)._1).
           map(a => (dir + Path.explode(a)).expand).toList
       }
       else Nil
     }
   }
 
   def pure_files(syntax: Outer_Syntax): List[Path] =
   {
     val pure_dir = Path.explode("~~/src/Pure")
     val roots =
       for { (name, _) <- Thy_Header.ml_roots }
       yield (pure_dir + Path.explode(name)).expand
     val files =
       for {
         (path, (_, theory)) <- roots zip Thy_Header.ml_roots
         file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
       } yield file
     roots ::: files
   }
 
   def theory_name(qualifier: String, theory: String): String =
     if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
       theory
     else Long_Name.qualify(qualifier, theory)
 
   def find_theory_node(theory: String): Option[Document.Node.Name] =
   {
     val thy_file = thy_path(Path.basic(Long_Name.base_name(theory)))
     val session = session_base.theory_qualifier(theory)
     val dirs =
       sessions_structure.get(session) match {
         case Some(info) => info.dirs
         case None => Nil
       }
     dirs.collectFirst({
       case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) })
   }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
     def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory)
 
     if (!Thy_Header.is_base_name(s)) theory_node
     else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
         case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node
       }
     }
   }
 
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     import_name(session_base.theory_qualifier(name), name.master_dir, s)
 
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
   def find_theory(file: JFile): Option[Document.Node.Name] =
   {
     for {
       qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
       theory_base <- proper_string(Thy_Header.theory_name(file.getName))
       theory = theory_name(qualifier, theory_base)
       theory_node <- find_theory_node(theory)
       if File.eq(theory_node.path.file, file)
     } yield theory_node
   }
 
   def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
   {
     val context_session = session_base.theory_qualifier(context_name)
     val context_dir =
       try { Some(context_name.master_dir_path) }
       catch { case ERROR(_) => None }
     (for {
       (session, (info, _))  <- sessions_structure.imports_graph.iterator
       dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
       theory <- Thy_Header.try_read_dir(dir).iterator
       if Completion.completed(s)(theory)
     } yield {
       if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
       else Long_Name.qualify(session, theory)
     }).toList.sorted
   }
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = name.path
     if (path.is_file) using(Scan.byte_reader(path.file))(f)
     else if (name.node == name.theory)
       error("Cannot load theory " + quote(name.theory))
     else error ("Cannot load theory file " + path)
   }
 
   def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
     start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
         val header = Thy_Header.read(reader, start, strict)
 
         val base_name = node_name.theory_base_name
         if (Long_Name.is_qualified(header.name)) {
           error("Bad theory name " + quote(header.name) + " with qualification" +
             Position.here(header.pos))
         }
         if (base_name != header.name) {
           error("Bad theory name " + quote(header.name) +
             " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
             Completion.report_theories(header.pos, List(base_name)))
         }
 
         val imports_pos =
           header.imports_pos.map({ case (s, pos) =>
             val name = import_name(node_name, s)
             if (Sessions.exclude_theory(name.theory_base_name))
               error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
             (name, pos)
           })
         Document.Node.Header(imports_pos, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }
     else Document.Node.no_header
   }
 
   def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
       strict: Boolean = true): Document.Node.Header =
     with_thy_reader(name, check_thy_reader(name, _, start, strict))
 
 
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   {
     val imports =
       if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
       else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
       else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
       else Nil
     if (imports.isEmpty) None
     else Some(Document.Node.Header(imports.map((_, Position.none))))
   }
 
 
   /* blobs */
 
   def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
     (for {
       (node_name, node) <- nodes.iterator
       if !session_base.loaded_theory(node_name)
       cmd <- node.load_commands.iterator
       name <- cmd.blobs_undefined.iterator
     } yield name).toList
 
 
   /* document changes */
 
   def parse_change(
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text],
       consolidate: List[Document.Node.Name]): Session.Change =
     Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
   def commit(change: Session.Change) { }
 
 
   /* theory and file dependencies */
 
   def dependencies(
       thys: List[(Document.Node.Name, Position.T)],
       progress: Progress = new Progress): Dependencies[Unit] =
     Dependencies.empty[Unit].require_thys((), thys, progress = progress)
 
   def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
     : Dependencies[Options] =
   {
     (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
       dependencies.require_thys(options,
         for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
         progress = progress)
     })
   }
 
   object Dependencies
   {
     def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty)
 
     private def show_path(names: List[Document.Node.Name]): String =
       names.map(name => quote(name.theory)).mkString(" via ")
 
     private def cycle_msg(names: List[Document.Node.Name]): String =
       "Cyclic dependency of " + show_path(names)
 
     private def required_by(initiators: List[Document.Node.Name]): String =
       if (initiators.isEmpty) ""
       else "\n(required by " + show_path(initiators.reverse) + ")"
   }
 
   final class Dependencies[A] private(
     rev_entries: List[Document.Node.Entry],
     seen: Map[Document.Node.Name, A])
   {
     private def cons(entry: Document.Node.Entry): Dependencies[A] =
       new Dependencies[A](entry :: rev_entries, seen)
 
     def require_thy(adjunct: A,
       thy: (Document.Node.Name, Position.T),
       initiators: List[Document.Node.Name] = Nil,
       progress: Progress = new Progress): Dependencies[A] =
     {
       val (name, pos) = thy
 
       def message: String =
         "The error(s) above occurred for theory " + quote(name.theory) +
           Dependencies.required_by(initiators) + Position.here(pos)
 
       if (seen.isDefinedAt(name)) this
       else {
         val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
         if (session_base.loaded_theory(name)) dependencies1
         else {
           try {
             if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators))
 
             progress.expose_interrupt()
             val header =
               try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
               catch { case ERROR(msg) => cat_error(msg, message) }
             val entry = Document.Node.Entry(name, header)
             dependencies1.require_thys(adjunct, header.imports_pos,
               initiators = name :: initiators, progress = progress).cons(entry)
           }
           catch {
             case e: Throwable =>
               dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))))
           }
         }
       }
     }
 
     def require_thys(adjunct: A,
         thys: List[(Document.Node.Name, Position.T)],
         progress: Progress = new Progress,
         initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
       (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
 
     def entries: List[Document.Node.Entry] = rev_entries.reverse
 
     def theories: List[Document.Node.Name] = entries.map(_.name)
     def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name)))
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 
     def check_errors: Dependencies[A] =
       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
 
     lazy val theory_graph: Document.Node.Name.Graph[Unit] =
     {
       val regular = theories.toSet
       val irregular =
         (for {
           entry <- entries.iterator
           imp <- entry.header.imports
           if !regular(imp)
         } yield imp).toSet
 
       Document.Node.Name.make_graph(
         irregular.toList.map(name => ((name, ()), Nil)) :::
         entries.map(entry => ((entry.name, ()), entry.header.imports)))
     }
 
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>
         val name = entry.name.theory
         val imports = entry.header.imports.map(_.theory)
 
         val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
         val graph2 = (graph1 /: imports)(_.add_edge(_, name))
 
         val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
         val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node)
         val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
 
         graph2.map_node(name, _ => syntax)
       })
 
     def loaded_files(pure: Boolean): List[(String, List[Path])] =
     {
       val loaded_files =
         theories.map(_.theory) zip
           Par_List.map((e: () => List[Path]) => e(),
             theories.map(name =>
               resources.loaded_files(loaded_theories.get_node(name.theory), name)))
 
       if (pure) {
         val pure_files = resources.pure_files(overall_syntax)
         loaded_files.map({ case (name, files) =>
           (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
       }
       else loaded_files
     }
 
     def imported_files: List[Path] =
     {
       val base_theories =
         loaded_theories.all_preds(theories.map(_.theory)).
           filter(session_base.loaded_theories.defined)
 
       base_theories.map(theory => session_base.known_theories(theory).name.path) :::
       base_theories.flatMap(session_base.known_loaded_files(_))
     }
 
     lazy val overall_syntax: Outer_Syntax =
       Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node))
 
     override def toString: String = entries.toString
   }
 }
diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala
+++ b/src/Pure/System/isabelle_tool.scala
@@ -1,188 +1,188 @@
 /*  Title:      Pure/System/isabelle_tool.scala
     Author:     Makarius
     Author:     Lars Hupel
 
 Isabelle system tools: external executables or internal Scala functions.
 */
 
 package isabelle
 
 import java.net.URLClassLoader
 import scala.reflect.runtime.universe
 import scala.tools.reflect.{ToolBox,ToolBoxError}
 
 
 object Isabelle_Tool
 {
   /* Scala source tools */
 
   abstract class Body extends Function[List[String], Unit]
 
   private def compile(path: Path): Body =
   {
     def err(msg: String): Nothing =
       cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
 
     val source = File.read(path)
 
     val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
     val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
 
     try {
       val symbol = tool_box.parse(source) match {
         case tree: universe.ModuleDef => tool_box.define(tree)
         case _ => err("Source does not describe a module (Scala object)")
       }
       tool_box.compile(universe.Ident(symbol))() match {
         case body: Body => body
         case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
       }
     }
     catch {
       case e: ToolBoxError =>
         if (tool_box.frontEnd.hasErrors) {
           val infos = tool_box.frontEnd.infos.toList
           val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
           err(msgs.mkString("\n"))
         }
         else
           err(e.toString)
     }
   }
 
 
   /* external tools */
 
   private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
 
   private def is_external(dir: Path, file_name: String): Boolean =
   {
     val file = (dir + Path.explode(file_name)).file
     try {
       file.isFile && file.canRead &&
         (file_name.endsWith(".scala") || file.canExecute) &&
         !file_name.endsWith("~") && !file_name.endsWith(".orig")
     }
     catch { case _: SecurityException => false }
   }
 
   private def list_external(): List[(String, String)] =
   {
     val Description = """.*\bDESCRIPTION: *(.*)""".r
     for {
       dir <- dirs() if dir.is_dir
       file_name <- File.read_dir(dir) if is_external(dir, file_name)
     } yield {
       val source = File.read(dir + Path.explode(file_name))
       val name = Library.perhaps_unsuffix(".scala", file_name)
       val description =
         split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
       (name, description)
     }
   }
 
   private def find_external(name: String): Option[List[String] => Unit] =
     dirs().collectFirst({
       case dir if is_external(dir, name + ".scala") =>
         compile(dir + Path.explode(name + ".scala"))
       case dir if is_external(dir, name) =>
         (args: List[String]) =>
           {
             val tool = dir + Path.explode(name)
             val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
             sys.exit(result.print_stdout.rc)
           }
     })
 
 
   /* internal tools */
 
   private lazy val internal_tools: List[Isabelle_Tool] =
     Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools)
 
   private def list_internal(): List[(String, String)] =
     for (tool <- internal_tools.toList)
       yield (tool.name, tool.description)
 
   private def find_internal(name: String): Option[List[String] => Unit] =
     internal_tools.collectFirst({
       case tool if tool.name == name =>
         args => Command_Line.tool { tool.body(args) }
       })
 
 
   /* command line entry point */
 
   def main(args: Array[String])
   {
     Command_Line.tool {
       args.toList match {
         case Nil | List("-?") =>
           val tool_descriptions =
             (list_external() ::: list_internal()).sortBy(_._1).
               map({ case (a, "") => a case (a, b) => a + " - " + b })
           Getopts("""
 Usage: isabelle TOOL [ARGS ...]
 
   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
 
 Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
         case tool_name :: tool_args =>
           find_external(tool_name) orElse find_internal(tool_name) match {
             case Some(tool) => tool(tool_args)
             case None => error("Unknown Isabelle tool: " + quote(tool_name))
           }
       }
     }
   }
 }
 
 sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
 
 class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
 
 class Tools extends Isabelle_Scala_Tools(
   Build.isabelle_tool,
   Build_Docker.isabelle_tool,
   Doc.isabelle_tool,
   Dump.isabelle_tool,
   Export.isabelle_tool,
   ML_Process.isabelle_tool,
   Mercurial.isabelle_tool,
   Mkroot.isabelle_tool,
   Options.isabelle_tool,
   Phabricator.isabelle_tool1,
   Phabricator.isabelle_tool2,
   Phabricator.isabelle_tool3,
   Phabricator.isabelle_tool4,
-  Present.isabelle_tool,
+  Presentation.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,
   Sessions.isabelle_tool,
   Scala_Project.isabelle_tool,
   Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,
   Update_Header.isabelle_tool,
   Update_Then.isabelle_tool,
   Update_Theorems.isabelle_tool,
   isabelle.vscode.Grammar.isabelle_tool,
   isabelle.vscode.Server.isabelle_tool)
 
 class Admin_Tools extends Isabelle_Scala_Tools(
   Build_CSDP.isabelle_tool,
   Build_Cygwin.isabelle_tool,
   Build_Doc.isabelle_tool,
   Build_E.isabelle_tool,
   Build_Fonts.isabelle_tool,
   Build_JDK.isabelle_tool,
   Build_PolyML.isabelle_tool1,
   Build_PolyML.isabelle_tool2,
   Build_SPASS.isabelle_tool,
   Build_SQLite.isabelle_tool,
   Build_Status.isabelle_tool,
   Build_VeriT.isabelle_tool,
   Build_Zipperposition.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool)
diff --git a/src/Pure/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala
+++ b/src/Pure/Thy/bibtex.scala
@@ -1,699 +1,699 @@
 /*  Title:      Pure/Thy/bibtex.scala
     Author:     Makarius
 
 BibTeX support.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.util.parsing.combinator.RegexParsers
 import scala.util.parsing.input.Reader
 
 
 object Bibtex
 {
   /** file format **/
 
   def is_bibtex(name: String): Boolean = name.endsWith(".bib")
 
   class File_Format extends isabelle.File_Format
   {
     val format_name: String = "bibtex"
     val file_ext: String = "bib"
 
     override def theory_suffix: String = "bibtex_file"
     override def theory_content(name: String): String =
       """theory "bib" imports Pure begin bibtex_file """ + quote(name) + """ end"""
 
-    override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+    override def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
     {
       val name = snapshot.node_name
       if (detect(name.node)) {
         val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
             File.write(bib, snapshot.node.source)
             Bibtex.html_output(List(bib), style = "unsort", title = title)
           }
-        Some(Present.Preview(title, content))
+        Some(Presentation.Preview(title, content))
       }
       else None
     }
   }
 
 
 
   /** bibtex errors **/
 
   def bibtex_errors(dir: Path, root_name: String): List[String] =
   {
     val log_path = dir + Path.explode(root_name).ext("blg")
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
       val Error2 = """^(.+)---line (\d+) of file (.+)""".r
       Line.logical_lines(File.read(log_path)).flatMap(line =>
         line match {
           case Error1(msg) => Some("Bibtex error: " + msg)
           case Error2(msg, Value.Int(l), file) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
               Some("Bibtex error" + Position.here(pos) + ":\n  " + msg)
             }
             else None
           case _ => None
         })
     }
     else Nil
   }
 
 
 
   /** check database **/
 
   def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) =
   {
     val chunks = parse(Line.normalize(database))
     var chunk_pos = Map.empty[String, Position.T]
     val tokens = new mutable.ListBuffer[(Token, Position.T)]
     var line = 1
     var offset = 1
 
     def make_pos(length: Int): Position.T =
       Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
 
     def advance_pos(tok: Token)
     {
       for (s <- Symbol.iterator(tok.source)) {
         if (Symbol.is_newline(s)) line += 1
         offset += 1
       }
     }
 
     def get_line_pos(l: Int): Position.T =
       if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
 
     for (chunk <- chunks) {
       val name = chunk.name
       if (name != "" && !chunk_pos.isDefinedAt(name)) {
         chunk_pos += (name -> make_pos(chunk.heading_length))
       }
       for (tok <- chunk.tokens) {
         tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
         advance_pos(tok)
       }
     }
 
     Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
     {
       File.write(tmp_dir + Path.explode("root.bib"),
         tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
       File.write(tmp_dir + Path.explode("root.aux"),
         "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
       Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
 
       val Error = """^(.*)---line (\d+) of file root.bib$""".r
       val Warning = """^Warning--(.+)$""".r
       val Warning_Line = """--line (\d+) of file root.bib$""".r
       val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
 
       val log_file = tmp_dir + Path.explode("root.blg")
       val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
 
       val (errors, warnings) =
         if (lines.isEmpty) (Nil, Nil)
         else {
           lines.zip(lines.tail ::: List("")).flatMap(
             {
               case (Error(msg, Value.Int(l)), _) =>
                 Some((true, (msg, get_line_pos(l))))
               case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
                 Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
               case (Warning(msg), Warning_Line(Value.Int(l))) =>
                 Some((false, (Word.capitalize(msg), get_line_pos(l))))
               case (Warning(msg), _) =>
                 Some((false, (Word.capitalize(msg), Position.none)))
               case _ => None
             }
           ).partition(_._1)
         }
       (errors.map(_._2), warnings.map(_._2))
     })
   }
 
   object Check_Database extends Scala.Fun("bibtex_check_database")
   {
     def apply(database: String): String =
     {
       import XML.Encode._
       YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
         check_database(database)))
     }
   }
 
 
 
   /** document model **/
 
   /* entries */
 
   def entries(text: String): List[Text.Info[String]] =
   {
     val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
     for (chunk <- Bibtex.parse(text)) {
       val end_offset = offset + chunk.source.length
       if (chunk.name != "" && !chunk.is_command)
         result += Text.Info(Text.Range(offset, end_offset), chunk.name)
       offset = end_offset
     }
     result.toList
   }
 
   def entries_iterator[A, B <: Document.Model](models: Map[A, B])
     : Iterator[Text.Info[(String, B)]] =
   {
     for {
       (_, model) <- models.iterator
       info <- model.bibtex_entries.iterator
     } yield info.map((_, model))
   }
 
 
   /* completion */
 
   def completion[A, B <: Document.Model](
     history: Completion.History, rendering: Rendering, caret: Text.Offset,
     models: Map[A, B]): Option[Completion.Result] =
   {
     for {
       Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
       name1 <- Completion.clean_name(name)
 
       original <- rendering.model.get_text(r)
       original1 <- Completion.clean_name(Library.perhaps_unquote(original))
 
       entries =
         (for {
           Text.Info(_, (entry, _)) <- entries_iterator(models)
           if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
         } yield entry).toList
       if entries.nonEmpty
 
       items =
         entries.sorted.map({
           case entry =>
             val full_name = Long_Name.qualify(Markup.CITATION, entry)
             val description = List(entry, "(BibTeX entry)")
             val replacement = quote(entry)
           Completion.Item(r, original, full_name, description, replacement, 0, false)
         }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
     } yield Completion.Result(r, original, false, items)
   }
 
 
 
   /** content **/
 
   private val months = List(
     "jan",
     "feb",
     "mar",
     "apr",
     "may",
     "jun",
     "jul",
     "aug",
     "sep",
     "oct",
     "nov",
     "dec")
   def is_month(s: String): Boolean = months.contains(s.toLowerCase)
 
   private val commands = List("preamble", "string")
   def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
 
   sealed case class Entry(
     kind: String,
     required: List[String],
     optional_crossref: List[String],
     optional_other: List[String])
   {
     val optional_standard: List[String] = List("url", "doi", "ee")
 
     def is_required(s: String): Boolean = required.contains(s.toLowerCase)
     def is_optional(s: String): Boolean =
       optional_crossref.contains(s.toLowerCase) ||
       optional_other.contains(s.toLowerCase) ||
       optional_standard.contains(s.toLowerCase)
 
     def fields: List[String] =
       required ::: optional_crossref ::: optional_other ::: optional_standard
 
     def template: String =
       "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
   }
 
   val known_entries: List[Entry] =
     List(
       Entry("Article",
         List("author", "title"),
         List("journal", "year"),
         List("volume", "number", "pages", "month", "note")),
       Entry("InProceedings",
         List("author", "title"),
         List("booktitle", "year"),
         List("editor", "volume", "number", "series", "pages", "month", "address",
           "organization", "publisher", "note")),
       Entry("InCollection",
         List("author", "title", "booktitle"),
         List("publisher", "year"),
         List("editor", "volume", "number", "series", "type", "chapter", "pages",
           "edition", "month", "address", "note")),
       Entry("InBook",
         List("author", "editor", "title", "chapter"),
         List("publisher", "year"),
         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
       Entry("Proceedings",
         List("title", "year"),
         List(),
         List("booktitle", "editor", "volume", "number", "series", "address", "month",
           "organization", "publisher", "note")),
       Entry("Book",
         List("author", "editor", "title"),
         List("publisher", "year"),
         List("volume", "number", "series", "address", "edition", "month", "note")),
       Entry("Booklet",
         List("title"),
         List(),
         List("author", "howpublished", "address", "month", "year", "note")),
       Entry("PhdThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry("MastersThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry("TechReport",
         List("author", "title", "institution", "year"),
         List(),
         List("type", "number", "address", "month", "note")),
       Entry("Manual",
         List("title"),
         List(),
         List("author", "organization", "address", "edition", "month", "year", "note")),
       Entry("Unpublished",
         List("author", "title", "note"),
         List(),
         List("month", "year")),
       Entry("Misc",
         List(),
         List(),
         List("author", "title", "howpublished", "month", "year", "note")))
 
   def get_entry(kind: String): Option[Entry] =
     known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
 
   def is_entry(kind: String): Boolean = get_entry(kind).isDefined
 
 
 
   /** tokens and chunks **/
 
   object Token
   {
     object Kind extends Enumeration
     {
       val COMMAND = Value("command")
       val ENTRY = Value("entry")
       val KEYWORD = Value("keyword")
       val NAT = Value("natural number")
       val STRING = Value("string")
       val NAME = Value("name")
       val IDENT = Value("identifier")
       val SPACE = Value("white space")
       val COMMENT = Value("ignored text")
       val ERROR = Value("bad input")
     }
   }
 
   sealed case class Token(kind: Token.Kind.Value, source: String)
   {
     def is_kind: Boolean =
       kind == Token.Kind.COMMAND ||
       kind == Token.Kind.ENTRY ||
       kind == Token.Kind.IDENT
     def is_name: Boolean =
       kind == Token.Kind.NAME ||
       kind == Token.Kind.IDENT
     def is_ignored: Boolean =
       kind == Token.Kind.SPACE ||
       kind == Token.Kind.COMMENT
     def is_malformed: Boolean =
       kind == Token.Kind.ERROR
     def is_open: Boolean =
       kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
   }
 
   case class Chunk(kind: String, tokens: List[Token])
   {
     val source = tokens.map(_.source).mkString
 
     private val content: Option[List[Token]] =
       tokens match {
         case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
           (body.init.filterNot(_.is_ignored), body.last) match {
             case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
             if tok.is_kind => Some(toks)
 
             case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
             if tok.is_kind => Some(toks)
 
             case _ => None
           }
         case _ => None
       }
 
     def name: String =
       content match {
         case Some(tok :: _) if tok.is_name => tok.source
         case _ => ""
       }
 
     def heading_length: Int =
       if (name == "") 1
       else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
     def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
   }
 
 
 
   /** parsing **/
 
   // context of partial line-oriented scans
   abstract class Line_Context
   case object Ignored extends Line_Context
   case object At extends Line_Context
   case class Item_Start(kind: String) extends Line_Context
   case class Item_Open(kind: String, end: String) extends Line_Context
   case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
 
   case class Delimited(quoted: Boolean, depth: Int)
   val Closed = Delimited(false, 0)
 
   private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
   private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
 
 
   // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
   // module @<Scan for and process a \.{.bib} command or database entry@>.
 
   object Parsers extends RegexParsers
   {
     /* white space and comments */
 
     override val whiteSpace = "".r
 
     private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
     private val spaces = rep(space)
 
 
     /* ignored text */
 
     private val ignored: Parser[Chunk] =
       rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
         case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
 
     private def ignored_line: Parser[(Chunk, Line_Context)] =
       ignored ^^ { case a => (a, Ignored) }
 
 
     /* delimited string: outermost "..." or {...} and body with balanced {...} */
 
     // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
     private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
       new Parser[(String, Delimited)]
       {
         require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0)
 
         def apply(in: Input) =
         {
           val start = in.offset
           val end = in.source.length
 
           var i = start
           var q = delim.quoted
           var d = delim.depth
           var finished = false
           while (!finished && i < end) {
             val c = in.source.charAt(i)
 
             if (c == '"' && d == 0) { i += 1; d = 1; q = true }
             else if (c == '"' && d == 1 && q) {
               i += 1; d = 0; q = false; finished = true
             }
             else if (c == '{') { i += 1; d += 1 }
             else if (c == '}') {
               if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
               else {i = start; finished = true }
             }
             else if (d > 0) i += 1
             else finished = true
           }
           if (i == start) Failure("bad input", in)
           else {
             val s = in.source.subSequence(start, i).toString
             Success((s, Delimited(q, d)), in.drop(i - start))
           }
         }
       }.named("delimited_depth")
 
     private def delimited: Parser[Token] =
       delimited_depth(Closed) ^?
         { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
 
     private def recover_delimited: Parser[Token] =
       """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
 
     def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
       delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
         (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
       recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
 
 
     /* other tokens */
 
     private val at = "@" ^^ keyword
 
     private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
 
     private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
 
     private val identifier =
       """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
 
     private val ident = identifier ^^ token(Token.Kind.IDENT)
 
     val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
 
 
     /* body */
 
     private val body =
       delimited | (recover_delimited | other_token)
 
     private def body_line(ctxt: Item) =
       if (ctxt.delim.depth > 0)
         delimited_line(ctxt)
       else
         delimited_line(ctxt) |
         other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
         ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
 
 
     /* items: command or entry */
 
     private val item_kind =
       identifier ^^ { case a =>
         val kind =
           if (is_command(a)) Token.Kind.COMMAND
           else if (is_entry(a)) Token.Kind.ENTRY
           else Token.Kind.IDENT
         Token(kind, a)
       }
 
     private val item_begin =
       "{" ^^ { case a => ("}", keyword(a)) } |
       "(" ^^ { case a => (")", keyword(a)) }
 
     private def item_name(kind: String) =
       kind.toLowerCase match {
         case "preamble" => failure("")
         case "string" => identifier ^^ token(Token.Kind.NAME)
         case _ => name
       }
 
     private val item_start =
       at ~ spaces ~ item_kind ~ spaces ^^
         { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
 
     private val item: Parser[Chunk] =
       (item_start ~ item_begin ~ spaces) into
         { case (kind, a) ~ ((end, b)) ~ c =>
             opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
               case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
 
     private val recover_item: Parser[Chunk] =
       at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
 
 
     /* chunks */
 
     val chunk: Parser[Chunk] = ignored | (item | recover_item)
 
     def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] =
     {
       ctxt match {
         case Ignored =>
           ignored_line |
           at ^^ { case a => (Chunk("", List(a)), At) }
 
         case At =>
           space ^^ { case a => (Chunk("", List(a)), ctxt) } |
           item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
           recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Start(kind) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
           recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Open(kind, end) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
           body_line(Item(kind, end, Closed)) |
           ignored_line
 
         case item_ctxt: Item =>
           body_line(item_ctxt) |
           ignored_line
 
         case _ => failure("")
       }
     }
   }
 
 
   /* parse */
 
   def parse(input: CharSequence): List[Chunk] =
     Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
       case Parsers.Success(result, _) => result
       case _ => error("Unexpected failure to parse input:\n" + input.toString)
     }
 
   def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) =
   {
     var in: Reader[Char] = Scan.char_reader(input)
     val chunks = new mutable.ListBuffer[Chunk]
     var ctxt = context
     while (!in.atEnd) {
       Parsers.parse(Parsers.chunk_line(ctxt), in) match {
         case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unepected failure to parse input:\n" + rest.source.toString)
       }
     }
     (chunks.toList, ctxt)
   }
 
 
 
   /** HTML output **/
 
   private val output_styles =
     List(
       "" -> "html-n",
       "plain" -> "html-n",
       "alpha" -> "html-a",
       "named" -> "html-n",
       "paragraph" -> "html-n",
       "unsort" -> "html-u",
       "unsortlist" -> "html-u")
 
   def html_output(bib: List[Path],
     title: String = "Bibliography",
     body: Boolean = false,
     citations: List[String] = List("*"),
     style: String = "",
     chronological: Boolean = false): String =
   {
     Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
     {
       /* database files */
 
       val bib_files = bib.map(_.drop_ext)
       val bib_names =
       {
         val names0 = bib_files.map(_.file_name)
         if (Library.duplicates(names0).isEmpty) names0
         else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
       }
 
       for ((a, b) <- bib_files zip bib_names) {
         File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
       }
 
 
       /* style file */
 
       val bst =
         output_styles.toMap.get(style) match {
           case Some(base) => base + (if (chronological) "c" else "") + ".bst"
           case None =>
             error("Bad style for bibtex HTML output: " + quote(style) +
               "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
         }
       File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
 
 
       /* result */
 
       val in_file = Path.explode("bib.aux")
       val out_file = Path.explode("bib.html")
 
       File.write(tmp_dir + in_file,
         bib_names.mkString("\\bibdata{", ",", "}\n") +
         citations.map(cite => "\\citation{" + cite + "}\n").mkString)
 
       Isabelle_System.bash(
         "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
           " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
           (if (chronological) " -c" else "") +
           (if (title != "") " -h " + Bash.string(title) + " " else "") +
           " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
         cwd = tmp_dir.file).check
 
       val html = File.read(tmp_dir + out_file)
 
       if (body) {
         cat_lines(
           split_lines(html).
             dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
             dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
       }
       else html
     })
   }
 }
diff --git a/src/Pure/Thy/file_format.scala b/src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala
+++ b/src/Pure/Thy/file_format.scala
@@ -1,97 +1,97 @@
 /*  Title:      Pure/Thy/file_format.scala
     Author:     Makarius
 
 Support for user-defined file formats.
 */
 
 package isabelle
 
 
 object File_Format
 {
   sealed case class Theory_Context(name: Document.Node.Name, content: String)
 
 
   /* registry */
 
   lazy val registry: Registry =
     new Registry(Isabelle_System.make_services(classOf[File_Format]))
 
   final class Registry private [File_Format](file_formats: List[File_Format])
   {
     override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
 
     def get(name: String): Option[File_Format] = file_formats.find(_.detect(name))
     def get(name: Document.Node.Name): Option[File_Format] = get(name.node)
     def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
     def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
 
     def start_session(session: isabelle.Session): Session =
       new Session(file_formats.map(_.start(session)).filterNot(_ == No_Agent))
   }
 
 
   /* session */
 
   final class Session private[File_Format](agents: List[Agent])
   {
     override def toString: String =
       agents.mkString("File_Format.Session(", ", ", ")")
 
     def prover_options(options: Options): Options =
       (options /: agents)({ case (opts, agent) => agent.prover_options(opts) })
 
     def stop_session { agents.foreach(_.stop) }
   }
 
   trait Agent
   {
     def prover_options(options: Options): Options = options
     def stop {}
   }
 
   object No_Agent extends Agent
 }
 
 abstract class File_Format extends Isabelle_System.Service
 {
   def format_name: String
   override def toString: String = "File_Format(" + format_name + ")"
 
   def file_ext: String
   def detect(name: String): Boolean = name.endsWith("." + file_ext)
 
 
   /* implicit theory context: name and content */
 
   def theory_suffix: String = ""
   def theory_content(name: String): String = ""
 
   def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
   {
     for {
       (_, ext_name) <- Thy_Header.split_file_name(name.node)
       if detect(ext_name) && theory_suffix.nonEmpty
     }
     yield {
       val thy_node = resources.append(name.node, Path.explode(theory_suffix))
       Document.Node.Name(thy_node, name.master_dir, ext_name)
     }
   }
 
   def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] =
   {
     for {
       (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == theory_suffix
       (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
       s <- proper_string(theory_content(ext_name))
     } yield s
   }
 
-  def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
+  def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = None
 
 
   /* PIDE session agent */
 
   def start(session: isabelle.Session): File_Format.Agent = File_Format.No_Agent
 }
diff --git a/src/Pure/Thy/present.scala b/src/Pure/Thy/presentation.scala
rename from src/Pure/Thy/present.scala
rename to src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/present.scala
+++ b/src/Pure/Thy/presentation.scala
@@ -1,488 +1,488 @@
 /*  Title:      Pure/Thy/present.scala
     Author:     Makarius
 
 Theory presentation: HTML and LaTeX documents.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedMap
 
 
-object Present
+object Presentation
 {
   /* 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 presentation = Presentation.Context.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:
     -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
     -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))),
         "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))
 
         build_documents(session, deps, store, progress = progress,
           presentation = presentation, verbose = true, verbose_latex = verbose_latex)
       }
     })
 }
diff --git a/src/Pure/Thy/sessions.scala b/src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala
+++ b/src/Pure/Thy/sessions.scala
@@ -1,1417 +1,1417 @@
 /*  Title:      Pure/Thy/sessions.scala
     Author:     Makarius
 
 Cumulative session information.
 */
 
 package isabelle
 
 import java.io.{File => JFile}
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
 
 import scala.collection.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
 object Sessions
 {
   /* session and theory names */
 
   val root_name: String = "ROOT"
   val theory_name: String = "Pure.Sessions"
 
   val UNSORTED = "Unsorted"
   val DRAFT = "Draft"
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
 
   def exclude_session(name: String): Boolean = name == "" || name == DRAFT
 
   def exclude_theory(name: String): Boolean =
     name == root_name || name == "README" || name == "index" || name == "bib"
 
 
   /* base info and source dependencies */
 
   object Base
   {
     def bootstrap(
         session_directories: Map[JFile, String],
         global_theories: Map[String, String]): Base =
       Base(
         session_directories = session_directories,
         global_theories = global_theories,
         overall_syntax = Thy_Header.bootstrap_syntax)
   }
 
   sealed case class Base(
     pos: Position.T = Position.none,
     doc_names: List[String] = Nil,
     session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
     session_theories: List[Document.Node.Name] = Nil,
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Document.Node.Name, Options)] = Nil,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil)
   {
     override def toString: String =
       "Sessions.Base(loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
     def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
 
     def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
     def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
       if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
     def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
       loaded_theory_syntax(name.theory)
 
     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base])
   {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
     def sources(name: String): List[SHA1.Digest] =
       session_bases(name).sources.map(_._2)
 
     def errors: List[String] =
       (for {
         (name, base) <- session_bases.iterator
         if base.errors.nonEmpty
       } yield cat_lines(base.errors) +
           "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos)
       ).toList
 
     def check_errors: Deps =
       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
   }
 
   def deps(sessions_structure: Structure,
       progress: Progress = new Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty): Deps =
   {
     var cache_sources = Map.empty[JFile, SHA1.Digest]
     def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
     {
       for {
         path <- paths
         file = path.file
         if cache_sources.isDefinedAt(file) || file.isFile
       }
       yield {
         cache_sources.get(file) match {
           case Some(digest) => (path, digest)
           case None =>
             val digest = SHA1.digest(file)
             cache_sources = cache_sources + (file -> digest)
             (path, digest)
         }
       }
     }
 
     val doc_names = Doc.doc_names()
 
     val bootstrap =
       Sessions.Base.bootstrap(
         sessions_structure.session_directories,
         sessions_structure.global_theories)
 
     val session_bases =
       (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
           val info = sessions_structure(session_name)
           try {
             val deps_base = info.deps_base(session_bases)
             val resources = new Resources(sessions_structure, deps_base)
 
             if (verbose || list_files) {
               val groups =
                 if (info.groups.isEmpty) ""
                 else info.groups.mkString(" (", " ", ")")
               progress.echo("Session " + info.chapter + "/" + info.name + groups)
             }
 
             val dependencies = resources.session_dependencies(info)
 
             val overall_syntax = dependencies.overall_syntax
 
             val session_theories =
               dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
 
             val theory_files = dependencies.theories.map(_.path)
 
             val (loaded_files, loaded_files_errors) =
               try {
                 if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil)
                 else (Nil, Nil)
               }
               catch { case ERROR(msg) => (Nil, List(msg)) }
 
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
             val imported_files = if (inlined_files) dependencies.imported_files else Nil
 
             if (list_files)
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
                 progress, overall_syntax.keywords, check_keywords, theory_files)
             }
 
             val session_graph_display: Graph_Display.Graph =
             {
               def session_node(name: String): Graph_Display.Node =
                 Graph_Display.Node("[" + name + "]", "session." + name)
 
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
                 val qualifier = deps_base.theory_qualifier(name)
                 if (qualifier == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(qualifier)
               }
 
               val required_sessions =
                 dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
                   .map(theory => deps_base.theory_qualifier(theory))
                   .filter(name => name != info.name && sessions_structure.defined(name))
 
               val required_subgraph =
                 sessions_structure.imports_graph
                   .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet)
                   .transitive_closure
                   .restrict(required_sessions.toSet)
                   .transitive_reduction_acyclic
 
               val graph0 =
                 (Graph_Display.empty_graph /: required_subgraph.topological_order)(
                   { case (g, session) =>
                       val a = session_node(session)
                       val bs = required_subgraph.imm_preds(session).toList.map(session_node)
                       ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
 
               (graph0 /: dependencies.entries)(
                 { case (g, entry) =>
                     val a = node(entry.name)
                     val bs = entry.header.imports.map(node).filterNot(_ == a)
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
             val known_theories =
               (deps_base.known_theories /:
                 dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _)
 
             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
 
             val import_errors =
             {
               val known_sessions =
                 sessions_structure.imports_requirements(List(session_name)).toSet
               for {
                 name <- dependencies.theories
                 qualifier = deps_base.theory_qualifier(name)
                 if !known_sessions(qualifier)
               } yield "Bad import of theory " + quote(name.toString) +
                 ": need to include sessions " + quote(qualifier) + " in ROOT"
             }
 
             val document_errors =
               info.document_theories.flatMap(
               {
                 case (thy, pos) =>
                   val parent_sessions =
                     if (sessions_structure.build_graph.defined(session_name)) {
                       sessions_structure.build_requirements(List(session_name))
                     }
                     else Nil
 
                   def err(msg: String): Option[String] =
                     Some(msg + " " + quote(thy) + Position.here(pos))
 
                   known_theories.get(thy).map(_.name) match {
                     case None => err("Unknown document theory")
                     case Some(name) =>
                       val qualifier = deps_base.theory_qualifier(name)
                       if (session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
                       else if (parent_sessions.contains(qualifier)) None
                       else if (dependencies.theories.contains(name)) None
                       else err("Document theory from other session not imported properly:")
                   }
               })
             val document_theories =
               info.document_theories.map({ case (thy, _) => known_theories(thy).name })
 
             val dir_errors =
             {
               val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
                   name <- session_theories.iterator
                   path = name.master_dir_path
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
               val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
               val errs1 =
                 for { (path1, name) <- bad }
                 yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString)
               val errs2 =
                 if (bad_dirs.isEmpty) Nil
                 else List("Implicit use of session directories: " + commas(bad_dirs))
               val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
               val errs4 =
                 (for {
                   name <- session_theories.iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
                 } yield "Incoherent theory file import:\n  " + name.path + " vs. \n  " + name1.path)
                 .toList
 
               errs1 ::: errs2 ::: errs3 ::: errs4
             }
 
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p
 
             val path_errors =
               try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
               catch { case ERROR(msg) => List(msg) }
 
             val bibtex_errors =
               try { info.bibtex_entries; Nil }
               catch { case ERROR(msg) => List(msg) }
 
             val base =
               Base(
                 pos = info.pos,
                 doc_names = doc_names,
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
                 session_theories = session_theories,
                 document_theories = document_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.theories_adjunct,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
                 errors = dependencies.errors ::: loaded_files_errors ::: import_errors :::
                   document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
                   bibtex_errors)
 
             session_bases + (info.name -> base)
           }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred in session " +
                 quote(info.name) + Position.here(info.pos))
           }
       })
 
     Deps(sessions_structure, session_bases)
   }
 
 
   /* base info */
 
   sealed case class Base_Info(
     session: String,
     sessions_structure: Structure,
     errors: List[String],
     base: Base,
     infos: List[Info])
   {
     def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
   }
 
   def base_info(options: Options,
     session: String,
     progress: Progress = new Progress,
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
     session_requirements: Boolean = false): Base_Info =
   {
     val full_sessions = load_structure(options, dirs = dirs)
 
     val selected_sessions =
       full_sessions.selection(Selection(sessions = session :: session_ancestor.toList))
     val info = selected_sessions(session)
     val ancestor = session_ancestor orElse info.parent
 
     val (session1, infos1) =
       if (session_requirements && ancestor.isDefined) {
         val deps = Sessions.deps(selected_sessions, progress = progress)
         val base = deps(session)
 
         val ancestor_loaded =
           deps.get(ancestor.get) match {
             case Some(ancestor_base)
             if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
               ancestor_base.loaded_theories.defined _
             case _ =>
               error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
           }
 
         val required_theories =
           for {
             thy <- base.loaded_theories.keys
             if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session
           }
           yield thy
 
         if (required_theories.isEmpty) (ancestor.get, Nil)
         else {
           val other_name = info.name + "_requirements(" + ancestor.get + ")"
           Isabelle_System.isabelle_tmp_prefix()
 
           (other_name,
             List(
               make_info(info.options,
                 dir_selected = false,
                 dir = Path.explode("$ISABELLE_TMP_PREFIX"),
                 chapter = info.chapter,
                 Session_Entry(
                   pos = info.pos,
                   name = other_name,
                   groups = info.groups,
                   path = ".",
                   parent = ancestor,
                   description = "Required theory imports from other sessions",
                   options = Nil,
                   imports = info.deps,
                   directories = Nil,
                   theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
                   document_theories = Nil,
                   document_files = Nil,
                   export_files = Nil))))
         }
       }
       else (session, Nil)
 
     val full_sessions1 =
       if (infos1.isEmpty) full_sessions
       else load_structure(options, dirs = dirs, infos = infos1)
 
     val selected_sessions1 =
       full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions))
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
     Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }
 
 
   /* cumulative session info */
 
   sealed case class Info(
     name: String,
     chapter: String,
     dir_selected: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,
     parent: Option[String],
     description: String,
     directories: List[Path],
     options: Options,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     document_theories: List[(String, Position.T)],
     document_files: List[(Path, Path)],
     export_files: List[(Path, Int, List[String])],
     meta_digest: SHA1.Digest)
   {
     def deps: List[String] = parent.toList ::: imports
 
     def deps_base(session_bases: String => Base): Base =
     {
       val parent_base = session_bases(parent.getOrElse(""))
       val imports_bases = imports.map(session_bases)
       parent_base.copy(
         known_theories =
           (parent_base.known_theories /:
             (for {
               base <- imports_bases.iterator
               (_, entry) <- base.known_theories.iterator
             } yield (entry.name.theory -> entry)))(_ + _),
         known_loaded_files =
           (parent_base.known_loaded_files /:
             imports_bases.iterator.map(_.known_loaded_files))(_ ++ _))
     }
 
     def dirs: List[Path] = dir :: directories
 
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def document_enabled: Boolean =
       options.string("document") match {
         case "" | "false" => false
         case "pdf" => true
         case doc => error("Bad document specification " + quote(doc))
       }
 
-    def documents_variants: List[Present.Document_Variant] =
+    def documents_variants: List[Presentation.Document_Variant] =
     {
       val variants =
         Library.space_explode(':', options.string("document_variants")).
-          map(Present.Document_Variant.parse)
+          map(Presentation.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
       if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
 
       variants
     }
 
-    def documents: List[Present.Document_Variant] =
+    def documents: List[Presentation.Document_Variant] =
     {
       val variants = documents_variants
       if (!document_enabled || document_files.isEmpty) Nil else variants
     }
 
     def document_output: Option[Path] =
       options.string("document_output") match {
         case "" => None
         case s => Some(dir + Path.explode(s))
       }
 
     def browser_info: Boolean = options.bool("browser_info")
 
     lazy val bibtex_entries: List[Text.Info[String]] =
       (for {
         (document_dir, file) <- document_files.iterator
         if Bibtex.is_bibtex(file.file_name)
         info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
       } yield info).toList
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 
     def is_afp: Boolean = chapter == AFP.chapter
     def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains)
   }
 
   def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String,
     entry: Session_Entry): Info =
   {
     try {
       val name = entry.name
 
       if (exclude_session(name)) error("Bad session name")
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
       val session_path = dir + Path.explode(entry.path)
       val directories = entry.directories.map(dir => session_path + Path.explode(dir))
 
       val session_options = options ++ entry.options
 
       val theories =
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts,
             thys.map({ case ((thy, pos), _) =>
               if (exclude_theory(thy))
                 error("Bad theory name " + quote(thy) + Position.here(pos))
               else (thy, pos) })) })
 
       val global_theories =
         for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
         yield {
           val thy_name = Path.explode(thy).file_name
           if (Long_Name.is_qualified(thy_name))
             error("Bad qualified name for global theory " +
               quote(thy_name) + Position.here(pos))
           else thy_name
         }
 
       val conditions =
         theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted.
           map(x => (x, Isabelle_System.getenv(x) != ""))
 
       val document_files =
         entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
 
       val export_files =
         entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
 
       val meta_digest =
         SHA1.digest(
           (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
             entry.theories_no_position, conditions, entry.document_theories, entry.document_files)
           .toString)
 
       Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
         entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, entry.document_theories, document_files,
         export_files, meta_digest)
     }
     catch {
       case ERROR(msg) =>
         error(msg + "\nThe error(s) above occurred in session entry " +
           quote(entry.name) + Position.here(entry.pos))
     }
   }
 
   object Selection
   {
     val empty: Selection = Selection()
     val all: Selection = Selection(all_sessions = true)
     def session(session: String): Selection = Selection(sessions = List(session))
   }
 
   sealed case class Selection(
     requirements: Boolean = false,
     all_sessions: Boolean = false,
     base_sessions: List[String] = Nil,
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
     sessions: List[String] = Nil)
   {
     def ++ (other: Selection): Selection =
       Selection(
         requirements = requirements || other.requirements,
         all_sessions = all_sessions || other.all_sessions,
         base_sessions = Library.merge(base_sessions, other.base_sessions),
         exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
   }
 
   def make(infos: List[Info]): Structure =
   {
     def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
       : Graph[String, Info] =
     {
       def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
       {
         if (!g.defined(parent))
           error("Bad " + kind + " session " + quote(parent) + " for " +
             quote(name) + Position.here(pos))
 
         try { g.add_edge_acyclic(parent, name) }
         catch {
           case exn: Graph.Cycles[_] =>
             error(cat_lines(exn.cycles.map(cycle =>
               "Cyclic session dependency of " +
                 cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
         }
       }
       (graph /: graph.iterator) {
         case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
       }
     }
 
     val info_graph =
       (Graph.string[Info] /: infos) {
         case (graph, info) =>
           if (graph.defined(info.name))
             error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
               Position.here(graph.get_node(info.name).pos))
           else graph.new_node(info.name, info)
       }
     val build_graph = add_edges(info_graph, "parent", _.parent)
     val imports_graph = add_edges(build_graph, "imports", _.imports)
 
     val session_positions: List[(String, Position.T)] =
       (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList
 
     val session_directories: Map[JFile, String] =
       (Map.empty[JFile, String] /:
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           dir <- info.dirs.iterator
         } yield (info, dir)))({ case (dirs, (info, dir)) =>
             val session = info.name
             val canonical_dir = dir.canonical_file
             dirs.get(canonical_dir) match {
               case Some(session1) =>
                 val info1 = info_graph.get_node(session1)
                 error("Duplicate use of directory " + dir +
                   "\n  for session " + quote(session1) + Position.here(info1.pos) +
                   "\n  vs. session " + quote(session) + Position.here(info.pos))
               case None => dirs + (canonical_dir -> session)
             }
           })
 
     val global_theories: Map[String, String] =
       (Thy_Header.bootstrap_global_theories.toMap /:
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           thy <- info.global_theories.iterator }
          yield (info, thy)))({ case (global, (info, thy)) =>
             val qualifier = info.name
             global.get(thy) match {
               case Some(qualifier1) if qualifier != qualifier1 =>
                 error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
               case _ => global + (thy -> qualifier)
             }
           })
 
     new Structure(
       session_positions, session_directories, global_theories, build_graph, imports_graph)
   }
 
   final class Structure private[Sessions](
       val session_positions: List[(String, Position.T)],
       val session_directories: Map[JFile, String],
       val global_theories: Map[String, String],
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
   {
     sessions_structure =>
 
     def dest_session_directories: List[(String, String)] =
       for ((file, session) <- session_directories.toList)
         yield (File.standard_path(file), session)
 
     lazy val chapters: SortedMap[String, List[Info]] =
       (SortedMap.empty[String, List[Info]] /: build_graph.iterator)(
         { case (chs, (_, (info, _))) =>
             chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) })
 
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
 
     def defined(name: String): Boolean = imports_graph.defined(name)
     def apply(name: String): Info = imports_graph.get_node(name)
     def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
 
     def theory_qualifier(name: String): String =
       global_theories.getOrElse(name, Long_Name.qualifier(name))
 
     def check_sessions(names: List[String])
     {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
 
     def check_sessions(sel: Selection): Unit =
       check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions)
 
     private def selected(graph: Graph[String, Info], sel: Selection): List[String] =
     {
       check_sessions(sel)
 
       val select_group = sel.session_groups.toSet
       val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions)
 
       val selected0 =
         if (sel.all_sessions) graph.keys
         else {
           (for {
             (name, (info, _)) <- graph.iterator
             if info.dir_selected || select_session(name) ||
               graph.get_node(name).groups.exists(select_group)
           } yield name).toList
         }
 
       if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
       else selected0
     }
 
     def selection(sel: Selection): Structure =
     {
       check_sessions(sel)
 
       val excluded =
       {
         val exclude_group = sel.exclude_session_groups.toSet
         val exclude_group_sessions =
           (for {
             (name, (info, _)) <- imports_graph.iterator
             if imports_graph.get_node(name).groups.exists(exclude_group)
           } yield name).toList
         imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
       }
 
       def restrict(graph: Graph[String, Info]): Graph[String, Info] =
       {
         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
       new Structure(
         session_positions, session_directories, global_theories,
         restrict(build_graph), restrict(imports_graph))
     }
 
     def selection(session: String): Structure = selection(Selection.session(session))
 
     def selection_deps(
       selection: Selection,
       progress: Progress = new Progress,
       loading_sessions: Boolean = false,
       inlined_files: Boolean = false,
       verbose: Boolean = false): Deps =
     {
       val deps =
         Sessions.deps(sessions_structure.selection(selection),
           progress = progress, inlined_files = inlined_files, verbose = verbose)
 
       if (loading_sessions) {
         val selection_size = deps.sessions_structure.build_graph.size
         if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...")
       }
 
       deps
     }
 
     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
     def build_topological_order: List[String] = build_graph.topological_order
 
     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
     def imports_topological_order: List[String] = imports_graph.topological_order
 
     def bibtex_entries: List[(String, List[String])] =
       build_topological_order.flatMap(name =>
         apply(name).bibtex_entries match {
           case Nil => None
           case entries => Some(name -> entries.map(_.info))
         })
 
     def session_chapters: List[(String, String)] =
       imports_topological_order.map(name => name -> apply(name).chapter)
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }
 
 
   /* parser */
 
   val ROOT: Path = Path.explode("ROOT")
   val ROOTS: Path = Path.explode("ROOTS")
 
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val DIRECTORIES = "directories"
   private val OPTIONS = "options"
   private val SESSIONS = "sessions"
   private val THEORIES = "theories"
   private val GLOBAL = "global"
   private val DOCUMENT_THEORIES = "document_theories"
   private val DOCUMENT_FILES = "document_files"
   private val EXPORT_FILES = "export_files"
 
   val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
       (DIRECTORIES, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
       (SESSIONS, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND) +
       (EXPORT_FILES, Keyword.QUASI_COMMAND)
 
   abstract class Entry
   sealed case class Chapter(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
     name: String,
     groups: List[String],
     path: String,
     parent: Option[String],
     description: String,
     options: List[Options.Spec],
     imports: List[String],
     directories: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_theories: List[(String, Position.T)],
     document_files: List[(String, String)],
     export_files: List[(String, Int, List[String])]) extends Entry
   {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
   }
 
   private object Parser extends Options.Parser
   {
     private val chapter: Parser[Chapter] =
     {
       val chapter_name = atom("chapter name", _.is_name)
 
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
     }
 
     private val session_entry: Parser[Session_Entry] =
     {
       val option =
         option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
           { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val theory_entry =
         position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
 
       val theories =
         $$$(THEORIES) ~!
           ((options | success(Nil)) ~ rep1(theory_entry)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
       val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x }
 
       val document_theories =
         $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x }
 
       val document_files =
         $$$(DOCUMENT_FILES) ~!
           ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
       val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
 
       val export_files =
         $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
           { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
       command(SESSION) ~!
         (position(session_name) ~
           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep(theories) ~
               (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~
               (rep(document_files) ^^ (x => x.flatten)) ~
               rep(export_files)))) ^^
         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l) }
     }
 
     def parse_root(path: Path): List[Entry] =
     {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
 
       parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
     }
   }
 
   def parse_root(path: Path): List[Entry] = Parser.parse_root(path)
 
   def parse_root_entries(path: Path): List[Session_Entry] =
     for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
     yield entry.asInstanceOf[Session_Entry]
 
   def read_root(options: Options, select: Boolean, path: Path): List[Info] =
   {
     var entry_chapter = UNSORTED
     val infos = new mutable.ListBuffer[Info]
     parse_root(path).foreach {
       case Chapter(name) => entry_chapter = name
       case entry: Session_Entry =>
         infos += make_info(options, select, path.dir, entry_chapter, entry)
     }
     infos.toList
   }
 
   def parse_roots(roots: Path): List[String] =
   {
     for {
       line <- split_lines(File.read(roots))
       if !(line == "" || line.startsWith("#"))
     } yield line
   }
 
 
   /* load sessions from certain directories */
 
   private def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   private def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else error("Bad session root directory: " + dir.toString)
 
   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
   {
     val default_dirs = Isabelle_System.components().filter(is_session_dir)
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }
 
   def load_structure(options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Info] = Nil): Structure =
   {
     def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
       load_root(select, dir) ::: load_roots(select, dir)
 
     def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] =
     {
       val root = dir + ROOT
       if (root.is_file) List((select, root)) else Nil
     }
 
     def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] =
     {
       val roots = dir + ROOTS
       if (roots.is_file) {
         for {
           entry <- parse_roots(roots)
           dir1 =
             try { check_session_dir(dir + Path.explode(entry)) }
             catch {
               case ERROR(msg) =>
                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
             }
           res <- load_dir(select, dir1)
         } yield res
       }
       else Nil
     }
 
     val roots =
       for {
         (select, dir) <- directories(dirs, select_dirs)
         res <- load_dir(select, check_session_dir(dir))
       } yield res
 
     val unique_roots =
       ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) =>
         val file = path.canonical_file
         m.get(file) match {
           case None => m + (file -> (select, path))
           case Some((select1, path1)) => m + (file -> (select1 || select, path1))
         }
       }).toList.map(_._2)
 
     make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", args =>
   {
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var requirements = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var dirs: List[Path] = Nil
     var session_groups: List[String] = Nil
     var exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle sessions [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -d DIR       include session directory
     -g NAME      select session group NAME
     -x NAME      exclude session NAME and all descendants
 
   Explore the structure of Isabelle sessions and print result names in
   topological order (on stdout).
 """,
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "R" -> (_ => requirements = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val options = Options.init()
 
     val selection =
       Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions,
         exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions,
         session_groups = session_groups, sessions = sessions)
     val sessions_structure =
       load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
 
     for (name <- sessions_structure.imports_topological_order) {
       Output.writeln(name, stdout = true)
     }
   })
 
 
 
   /** heap file with SHA1 digest **/
 
   private val sha1_prefix = "SHA1:"
 
   def read_heap_digest(heap: Path): Option[String] =
   {
     if (heap.is_file) {
       using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>
       {
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length
         if (len >= n) {
           file.position(len - n)
 
           val buf = ByteBuffer.allocate(n)
           var i = 0
           var m = 0
           do {
             m = file.read(buf)
             if (m != -1) i += m
           }
           while (m != -1 && n > i)
 
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
             val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
             if (prefix == sha1_prefix) Some(s) else None
           }
           else None
         }
         else None
       })
     }
     else None
   }
 
   def write_heap_digest(heap: Path): String =
     read_heap_digest(heap) match {
       case None =>
         val s = SHA1.digest(heap).rep
         File.append(heap, sha1_prefix + s)
         s
       case Some(s) => s
     }
 
 
 
   /** persistent store **/
 
   object Session_Info
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
 
     // Build_Log.Session_Info
     val session_timing = SQL.Column.bytes("session_timing")
     val command_timings = SQL.Column.bytes("command_timings")
     val theory_timings = SQL.Column.bytes("theory_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val task_statistics = SQL.Column.bytes("task_statistics")
     val errors = SQL.Column.bytes("errors")
     val build_log_columns =
       List(session_name, session_timing, command_timings, theory_timings,
         ml_statistics, task_statistics, errors)
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
     val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
     val return_code = SQL.Column.int("return_code")
     val build_columns = List(sources, input_heaps, output_heap, return_code)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
   }
 
   def store(options: Options): Store = new Store(options)
 
   class Store private[Sessions](val options: Options)
   {
     store =>
 
     override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
     val xml_cache: XML.Cache = XML.make_cache()
     val xz_cache: XZ.Cache = XZ.make_cache()
 
 
     /* directories */
 
     val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
     val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
 
     def system_heaps: Boolean = options.bool("system_heaps")
 
     val output_dir: Path =
       if (system_heaps) system_output_dir else user_output_dir
 
     val input_dirs: List[Path] =
       if (system_heaps) List(system_output_dir)
       else List(user_output_dir, system_output_dir)
 
     def presentation_dir: Path =
       if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
       else Path.explode("$ISABELLE_BROWSER_INFO")
 
 
     /* file names */
 
     def heap(name: String): Path = Path.basic(name)
     def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
     def log(name: String): Path = Path.basic("log") + Path.basic(name)
     def log_gz(name: String): Path = log(name).ext("gz")
 
     def output_heap(name: String): Path = output_dir + heap(name)
     def output_database(name: String): Path = output_dir + database(name)
     def output_log(name: String): Path = output_dir + log(name)
     def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
     def prepare_output_dir() { Isabelle_System.make_directory(output_dir + Path.basic("log")) }
 
 
     /* heap */
 
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
     def find_heap_digest(name: String): Option[String] =
       find_heap(name).flatMap(read_heap_digest)
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
         error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
           cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
 
 
     /* database */
 
     def database_server: Boolean = options.bool("build_database_server")
 
     def open_database_server(): SQL.Database =
       PostgreSQL.open_database(
         user = options.string("build_database_user"),
         password = options.string("build_database_password"),
         database = options.string("build_database_name"),
         host = options.string("build_database_host"),
         port = options.int("build_database_port"),
         ssh =
           options.proper_string("build_database_ssh_host").map(ssh_host =>
             SSH.open_session(options,
               host = ssh_host,
               user = options.string("build_database_ssh_user"),
               port = options.int("build_database_ssh_port"))),
         ssh_close = true)
 
     def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
       def check(db: SQL.Database): Option[SQL.Database] =
         if (output || session_info_exists(db)) Some(db) else { db.close; None }
 
       if (database_server) check(open_database_server())
       else if (output) Some(SQLite.open_database(output_database(name)))
       else {
         (for {
           dir <- input_dirs.view
           path = dir + database(name) if path.is_file
           db <- check(SQLite.open_database(path))
         } yield db).headOption
       }
     }
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
       try_open_database(name, output = output) getOrElse
         error("Missing build database for session " + quote(name))
 
     def clean_output(name: String): (Boolean, Boolean) =
     {
       val relevant_db =
         database_server &&
         {
           try_open_database(name) match {
             case Some(db) =>
               try {
                 db.transaction {
                   val relevant_db = session_info_defined(db, name)
                   init_session_info(db, name)
                   relevant_db
                 }
               } finally { db.close }
             case None => false
           }
         }
 
       val del =
         for {
           dir <-
             (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
           file <- List(heap(name), database(name), log(name), log_gz(name))
           path = dir + file if path.is_file
         } yield path.file.delete
 
       val relevant = relevant_db || del.nonEmpty
       val ok = del.forall(b => b)
       (relevant, ok)
     }
 
 
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
         Session_Info.session_name.where_equal(name)))(stmt =>
       {
         val res = stmt.execute_query()
         if (!res.next()) Bytes.empty else res.bytes(column)
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
       Properties.uncompress(
         read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache))
 
 
     /* session info */
 
     def init_session_info(db: SQL.Database, name: String)
     {
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
 
         db.create_table(Export.Data.table)
         db.using_statement(
           Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
       }
     }
 
     def session_info_exists(db: SQL.Database): Boolean =
     {
       val tables = db.tables
       tables.contains(Session_Info.table.name) &&
       tables.contains(Export.Data.table.name)
     }
 
     def session_info_defined(db: SQL.Database, name: String): Boolean =
       db.transaction {
         session_info_exists(db) &&
         {
           db.using_statement(
             Session_Info.table.select(List(Session_Info.session_name),
               Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
         }
       }
 
     def write_session_info(
       db: SQL.Database,
       name: String,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info)
     {
       db.transaction {
         db.using_statement(Session_Info.table.insert())(stmt =>
         {
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
           stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
           stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
           stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache)
           stmt.string(8) = build.sources
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
           stmt.int(11) = build.return_code
           stmt.execute()
         })
       }
     }
 
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
       Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache))
 
     def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.command_timings)
 
     def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.theory_timings)
 
     def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.ml_statistics)
 
     def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.task_statistics)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache)
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     {
       if (db.tables.contains(Session_Info.table.name)) {
         db.using_statement(Session_Info.table.select(Session_Info.build_columns,
           Session_Info.session_name.where_equal(name)))(stmt =>
         {
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
             Some(
               Build.Session_Info(
                 res.string(Session_Info.sources),
                 split_lines(res.string(Session_Info.input_heaps)),
                 res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
                 res.int(Session_Info.return_code)))
           }
         })
       }
       else None
     }
   }
 }
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,971 +1,971 @@
 /*  Title:      Pure/Tools/build.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Build and manage Isabelle sessions.
 */
 
 package isabelle
 
 
 import scala.collection.{SortedSet, mutable}
 import scala.annotation.tailrec
 
 
 object Build
 {
   /** auxiliary **/
 
   /* persistent build info */
 
   sealed case class Session_Info(
     sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
   {
     def ok: Boolean = return_code == 0
   }
 
 
   /* queue with scheduling information */
 
   private object Queue
   {
     type Timings = (List[Properties.T], Double)
 
     def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
     {
       val no_timings: Timings = (Nil, 0.0)
 
       store.try_open_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
           {
             progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {
             val command_timings = store.read_command_timings(db, session_name)
             val session_timing =
               store.read_session_timing(db, session_name) match {
                 case Markup.Elapsed(t) => t
                 case _ => 0.0
               }
             (command_timings, session_timing)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
           finally { db.close }
       }
     }
 
     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
       val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(session_name: String): Double =
       {
         if (maximals.contains(session_name)) timing(session_name)
         else {
           val descendants = sessions_structure.build_descendants(List(session_name)).toSet
           val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => !timing.isDefinedAt(p))) None
             else Some(ps.map(timing(_)).sum)
           })).max
         }
       }
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
       : Queue =
     {
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
         def compare_timing(name1: String, name2: String): Int =
         {
           val t1 = session_timing(name1)
           val t2 = session_timing(name2)
           if (t1 == 0.0 || t2 == 0.0) 0
           else t1 compare t2
         }
 
         def compare(name1: String, name2: String): Int =
           compare_timing(name2, name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }
             case ord => ord
           }
       }
 
       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
     }
   }
 
   private class Queue(
     graph: Graph[String, Sessions.Info],
     order: SortedSet[String],
     val command_timings: String => List[Properties.T])
   {
     def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
       new Queue(graph.del_node(name),
         order - name,  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
         command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
       val it = order.iterator.dropWhile(name =>
         skip(name)
           || !graph.defined(name)  // FIXME scala-2.10.0 .. 2.12.4 TreeSet problem!?
           || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
       else None
     }
   }
 
 
   /* PIDE protocol handler */
 
   /* job: running prover process */
 
   private class Job(progress: Progress,
     session_name: String,
     val info: Sessions.Info,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_store: Boolean,
-    presentation: Present.Context,
+    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) {
               if (info.documents.nonEmpty) {
                 val document_progress =
                   new Progress {
                     override def echo(msg: String): Unit =
                       document_output.synchronized { document_output += msg }
                     override def echo_document(path: Path): Unit =
                       progress.echo_document(path)
                   }
-                Present.build_documents(session_name, deps, store, verbose = verbose,
+                Presentation.build_documents(session_name, deps, store, verbose = verbose,
                   verbose_latex = true, progress = document_progress)
               }
               if (presentation.enabled(info)) {
-                val dir = Present.session_html(session_name, deps, store, presentation)
+                val dir = Presentation.session_html(session_name, deps, store, presentation)
                 if (verbose) progress.echo("Browser info at " + dir.absolute)
               }
             }
             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)
     }
   }
 
 
 
   /** build with results **/
 
   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   {
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
     val rc: Int =
       (0 /: results.iterator.map(
         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
     def ok: Boolean = rc == 0
 
     override def toString: String = rc.toString
   }
 
   def session_finished(session_name: String, process_result: Process_Result): String =
     "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
 
   def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
   {
     val props = build_log.session_timing
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
     val timing = Markup.Timing_Properties.parse(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }
 
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
-    presentation: Present.Context = Present.Context.none,
+    presentation: Presentation.Context = Presentation.Context.none,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
     verbose: Boolean = false,
     export_files: Boolean = false): Results =
   {
     val build_options =
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
         "pide_reports=false"
 
     val store = Sessions.store(build_options)
 
     Isabelle_Fonts.init()
 
 
     /* session selection and dependencies */
 
     val full_sessions =
       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
     {
       val digests =
         full_sessions(session_name).meta_digest ::
         deps.sources(session_name) :::
         deps.imported_sources(session_name)
       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     }
 
     val deps =
     {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.try_open_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
             })
 
         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
           progress = progress, inlined_files = true).check_errors
       }
       else deps0
     }
 
 
     /* check unknown files */
 
     if (check_unknown_files) {
       val source_files =
         (for {
           (_, base) <- deps.session_bases.iterator
           (path, _) <- base.sources.iterator
         } yield path).toList
       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
       val unknown_files =
         Mercurial.check_files(source_files)._2.
           filterNot(path => exclude_files.contains(path.canonical_file))
       if (unknown_files.nonEmpty) {
         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }
 
 
     /* main build process */
 
     val queue = Queue(progress, deps.sessions_structure, store)
 
     store.prepare_output_dir()
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions.imports_selection(selection))) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
           else progress.echo(name + " FAILED to clean")
         }
       }
     }
 
     // scheduler loop
     case class Result(
       current: Boolean,
       heap_digest: Option[String],
       process: Option[Process_Result],
       info: Sessions.Info)
     {
       def ok: Boolean =
         process match {
           case None => false
           case Some(res) => res.rc == 0
         }
     }
 
     def sleep()
     {
       Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
     }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
     @tailrec def loop(
       pending: Queue,
       running: Map[String, (List[String], Job)],
       results: Map[String, Result]): Map[String, Result] =
     {
       def used_node(i: Int): Boolean =
         running.iterator.exists(
           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
 
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
           for ((_, (_, job)) <- running) job.terminate
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
             val (process_result, heap_digest) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail =
             {
               val tail = job.info.options.int("process_output_tail")
               process_result.copy(
                 out_lines =
                   "(see also " + store.output_log(session_name).file.toString + ")" ::
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
             val build_log =
               Build_Log.Log_File(session_name, process_result.out_lines).
                 parse_session_info(
                   command_timings = true,
                   theory_timings = true,
                   ml_statistics = true,
                   task_statistics = true)
 
             // write log file
             if (process_result.ok) {
               File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
             }
             else File.write(store.output_log(session_name), terminate_lines(log_lines))
 
             // write database
             using(store.open_database(session_name, output = true))(db =>
               store.write_session_info(db, session_name,
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
                   Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
                     process_result.rc)))
 
             // messages
             process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok) {
               if (verbose) progress.echo(session_timing(session_name, build_log))
               progress.echo(session_finished(session_name, process_result))
             }
             else {
               progress.echo(session_name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)
             }
 
             loop(pending - session_name, running - session_name,
               results +
                 (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt) match {
               case Some((session_name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
                 val (current, heap_digest) =
                 {
                   store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
                           val heap_digest = store.find_heap_digest(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, session_name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_digest &&
                             !(do_store && heap_digest.isEmpty)
                           (current, heap_digest)
                         case None => (false, None)
                       }
                     case None => (false, None)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
 
                 if (all_current)
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
                   store.clean_output(session_name)
                   using(store.open_database(session_name, output = true))(
                     store.init_session_info(_, session_name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Job(progress, session_name, info, deps, store, do_store, presentation,
                       verbose, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
                     results + (session_name -> Result(false, heap_digest, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)
         }
       }
     }
 
 
     /* build results */
 
     val results0 =
       if (deps.is_empty) {
         progress.echo_warning("Nothing to build")
         Map.empty[String, Result]
       }
       else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
     val results =
       new Results(
         (for ((name, result) <- results0.iterator)
           yield (name, (result.process, result.info))).toMap)
 
     if (export_files) {
       for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
               progress = if (verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
         }
       }
     }
 
     if (results.rc != 0 && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator
           if !results(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
 
     /* global browser info */
 
     if (!no_build) {
       val browser_chapters =
         (for {
           (name, result) <- results0.iterator
           if result.ok
           info = full_sessions(name)
           if presentation.enabled(info)
         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
 
       val dir = presentation.dir(store)
 
       for ((chapter, entries) <- browser_chapters)
-        Present.update_chapter_index(dir, chapter, entries)
+        Presentation.update_chapter_index(dir, chapter, entries)
 
-      if (browser_chapters.nonEmpty) Present.make_global_index(dir)
+      if (browser_chapters.nonEmpty) Presentation.make_global_index(dir)
     }
 
     results
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
-    var presentation = Present.Context.none
+    var presentation = Presentation.Context.none
     var requirements = false
     var soft_build = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var build_heap = false
     var clean_build = false
     var dirs: List[Path] = Nil
     var export_files = false
     var fresh_build = false
     var session_groups: List[String] = Nil
     var max_jobs = 1
     var check_keywords: Set[String] = Set.empty
     var list_files = false
     var no_build = false
     var options = Options.init(opts = build_options)
     var verbose = false
     var exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
     -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- test dependencies only
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.prefix_lines("  ",  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
-      "P:" -> (arg => presentation = Present.Context.make(arg)),
+      "P:" -> (arg => presentation = Presentation.Context.make(arg)),
       "R" -> (_ => requirements = true),
       "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e" -> (_ => export_files = true),
       "f" -> (_ => fresh_build = true),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val progress = new Console_Progress(verbose = verbose)
 
     val start_date = Date.now()
 
     if (verbose) {
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
 
     val results =
       progress.interrupt_handler {
         build(options,
           selection = Sessions.Selection(
             requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
             exclude_session_groups = exclude_session_groups,
             exclude_sessions = exclude_sessions,
             session_groups = session_groups,
             sessions = sessions),
           presentation = presentation,
           progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
           build_heap = build_heap,
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,
           fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files)
       }
     val end_date = Date.now()
     val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
     }
 
     val total_timing =
       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)
 
     sys.exit(results.rc)
   })
 
 
   /* build logic image */
 
   def build_logic(options: Options, logic: String,
     progress: Progress = new Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val selection = Sessions.Selection.session(logic)
     val rc =
       if (!fresh && build(options, selection = selection,
             build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, selection = selection, progress = progress,
           build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
       }
     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
 }
diff --git a/src/Pure/build-jars b/src/Pure/build-jars
--- a/src/Pure/build-jars
+++ b/src/Pure/build-jars
@@ -1,318 +1,318 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # build-jars - build Isabelle/Scala
 #
 # Requires proper Isabelle settings environment.
 
 ## sources
 
 declare -a SOURCES=(
   src/HOL/Tools/Nitpick/kodkod.scala
   src/Pure/Admin/afp.scala
   src/Pure/Admin/build_csdp.scala
   src/Pure/Admin/build_cygwin.scala
   src/Pure/Admin/build_doc.scala
   src/Pure/Admin/build_e.scala
   src/Pure/Admin/build_fonts.scala
   src/Pure/Admin/build_history.scala
   src/Pure/Admin/build_jdk.scala
   src/Pure/Admin/build_log.scala
   src/Pure/Admin/build_polyml.scala
   src/Pure/Admin/build_release.scala
   src/Pure/Admin/build_spass.scala
   src/Pure/Admin/build_sqlite.scala
   src/Pure/Admin/build_status.scala
   src/Pure/Admin/build_verit.scala
   src/Pure/Admin/build_zipperposition.scala
   src/Pure/Admin/check_sources.scala
   src/Pure/Admin/ci_profile.scala
   src/Pure/Admin/components.scala
   src/Pure/Admin/isabelle_cronjob.scala
   src/Pure/Admin/isabelle_devel.scala
   src/Pure/Admin/jenkins.scala
   src/Pure/Admin/other_isabelle.scala
   src/Pure/Concurrent/consumer_thread.scala
   src/Pure/Concurrent/counter.scala
   src/Pure/Concurrent/delay.scala
   src/Pure/Concurrent/event_timer.scala
   src/Pure/Concurrent/future.scala
   src/Pure/Concurrent/isabelle_thread.scala
   src/Pure/Concurrent/mailbox.scala
   src/Pure/Concurrent/par_list.scala
   src/Pure/Concurrent/synchronized.scala
   src/Pure/GUI/color_value.scala
   src/Pure/GUI/gui.scala
   src/Pure/GUI/gui_thread.scala
   src/Pure/GUI/popup.scala
   src/Pure/GUI/wrap_panel.scala
   src/Pure/General/antiquote.scala
   src/Pure/General/bytes.scala
   src/Pure/General/cache.scala
   src/Pure/General/codepoint.scala
   src/Pure/General/comment.scala
   src/Pure/General/completion.scala
   src/Pure/General/csv.scala
   src/Pure/General/date.scala
   src/Pure/General/exn.scala
   src/Pure/General/file.scala
   src/Pure/General/file_watcher.scala
   src/Pure/General/graph.scala
   src/Pure/General/graph_display.scala
   src/Pure/General/graphics_file.scala
   src/Pure/General/http.scala
   src/Pure/General/json.scala
   src/Pure/General/linear_set.scala
   src/Pure/General/logger.scala
   src/Pure/General/long_name.scala
   src/Pure/General/mailman.scala
   src/Pure/General/mercurial.scala
   src/Pure/General/multi_map.scala
   src/Pure/General/output.scala
   src/Pure/General/path.scala
   src/Pure/General/position.scala
   src/Pure/General/pretty.scala
   src/Pure/General/properties.scala
   src/Pure/General/rdf.scala
   src/Pure/General/scan.scala
   src/Pure/General/sha1.scala
   src/Pure/General/sql.scala
   src/Pure/General/ssh.scala
   src/Pure/General/symbol.scala
   src/Pure/General/time.scala
   src/Pure/General/timing.scala
   src/Pure/General/untyped.scala
   src/Pure/General/url.scala
   src/Pure/General/utf8.scala
   src/Pure/General/uuid.scala
   src/Pure/General/value.scala
   src/Pure/General/word.scala
   src/Pure/General/xz.scala
   src/Pure/Isar/document_structure.scala
   src/Pure/Isar/keyword.scala
   src/Pure/Isar/line_structure.scala
   src/Pure/Isar/outer_syntax.scala
   src/Pure/Isar/parse.scala
   src/Pure/Isar/token.scala
   src/Pure/ML/ml_console.scala
   src/Pure/ML/ml_lex.scala
   src/Pure/ML/ml_process.scala
   src/Pure/ML/ml_statistics.scala
   src/Pure/ML/ml_syntax.scala
   src/Pure/PIDE/byte_message.scala
   src/Pure/PIDE/command.scala
   src/Pure/PIDE/command_span.scala
   src/Pure/PIDE/document.scala
   src/Pure/PIDE/document_id.scala
   src/Pure/PIDE/document_status.scala
   src/Pure/PIDE/editor.scala
   src/Pure/PIDE/headless.scala
   src/Pure/PIDE/line.scala
   src/Pure/PIDE/markup.scala
   src/Pure/PIDE/markup_tree.scala
   src/Pure/PIDE/protocol.scala
   src/Pure/PIDE/protocol_handlers.scala
   src/Pure/PIDE/protocol_message.scala
   src/Pure/PIDE/prover.scala
   src/Pure/PIDE/query_operation.scala
   src/Pure/PIDE/rendering.scala
   src/Pure/PIDE/resources.scala
   src/Pure/PIDE/session.scala
   src/Pure/PIDE/text.scala
   src/Pure/PIDE/xml.scala
   src/Pure/PIDE/yxml.scala
   src/Pure/ROOT.scala
   src/Pure/System/bash.scala
   src/Pure/System/command_line.scala
   src/Pure/System/cygwin.scala
   src/Pure/System/distribution.scala
   src/Pure/System/executable.scala
   src/Pure/System/getopts.scala
   src/Pure/System/isabelle_charset.scala
   src/Pure/System/isabelle_fonts.scala
   src/Pure/System/isabelle_platform.scala
   src/Pure/System/isabelle_process.scala
   src/Pure/System/isabelle_system.scala
   src/Pure/System/isabelle_tool.scala
   src/Pure/System/java_statistics.scala
   src/Pure/System/linux.scala
   src/Pure/System/mingw.scala
   src/Pure/System/numa.scala
   src/Pure/System/options.scala
   src/Pure/System/platform.scala
   src/Pure/System/posix_interrupt.scala
   src/Pure/System/process_result.scala
   src/Pure/System/progress.scala
   src/Pure/System/scala.scala
   src/Pure/System/system_channel.scala
   src/Pure/System/tty_loop.scala
   src/Pure/Thy/bibtex.scala
   src/Pure/Thy/export.scala
   src/Pure/Thy/export_theory.scala
   src/Pure/Thy/file_format.scala
   src/Pure/Thy/html.scala
   src/Pure/Thy/latex.scala
-  src/Pure/Thy/present.scala
+  src/Pure/Thy/presentation.scala
   src/Pure/Thy/sessions.scala
   src/Pure/Thy/thy_element.scala
   src/Pure/Thy/thy_header.scala
   src/Pure/Thy/thy_syntax.scala
   src/Pure/Tools/build.scala
   src/Pure/Tools/build_docker.scala
   src/Pure/Tools/check_keywords.scala
   src/Pure/Tools/debugger.scala
   src/Pure/Tools/doc.scala
   src/Pure/Tools/dump.scala
   src/Pure/Tools/fontforge.scala
   src/Pure/Tools/main.scala
   src/Pure/Tools/mkroot.scala
   src/Pure/Tools/phabricator.scala
   src/Pure/Tools/print_operation.scala
   src/Pure/Tools/profiling_report.scala
   src/Pure/Tools/scala_project.scala
   src/Pure/Tools/server.scala
   src/Pure/Tools/server_commands.scala
   src/Pure/Tools/simplifier_trace.scala
   src/Pure/Tools/spell_checker.scala
   src/Pure/Tools/task_statistics.scala
   src/Pure/Tools/update.scala
   src/Pure/Tools/update_cartouches.scala
   src/Pure/Tools/update_comments.scala
   src/Pure/Tools/update_header.scala
   src/Pure/Tools/update_then.scala
   src/Pure/Tools/update_theorems.scala
   src/Pure/library.scala
   src/Pure/pure_thy.scala
   src/Pure/term.scala
   src/Pure/term_xml.scala
   src/Pure/thm_name.scala
   src/Tools/Graphview/graph_file.scala
   src/Tools/Graphview/graph_panel.scala
   src/Tools/Graphview/graphview.scala
   src/Tools/Graphview/layout.scala
   src/Tools/Graphview/main_panel.scala
   src/Tools/Graphview/metrics.scala
   src/Tools/Graphview/model.scala
   src/Tools/Graphview/mutator.scala
   src/Tools/Graphview/mutator_dialog.scala
   src/Tools/Graphview/mutator_event.scala
   src/Tools/Graphview/popups.scala
   src/Tools/Graphview/shapes.scala
   src/Tools/Graphview/tree_panel.scala
   src/Tools/VSCode/src/build_vscode.scala
   src/Tools/VSCode/src/channel.scala
   src/Tools/VSCode/src/document_model.scala
   src/Tools/VSCode/src/dynamic_output.scala
   src/Tools/VSCode/src/grammar.scala
   src/Tools/VSCode/src/preview_panel.scala
   src/Tools/VSCode/src/protocol.scala
   src/Tools/VSCode/src/server.scala
   src/Tools/VSCode/src/state_panel.scala
   src/Tools/VSCode/src/vscode_rendering.scala
   src/Tools/VSCode/src/vscode_resources.scala
   src/Tools/VSCode/src/vscode_spell_checker.scala
 )
 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS]"
   echo
   echo "  Options are:"
   echo "    -f           fresh build"
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
 
 
 ## process command line
 
 # options
 
 FRESH=""
 
 while getopts "f" OPT
 do
   case "$OPT" in
     f)
       FRESH=true
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 [ "$#" -ne 0 ] && usage
 
 
 ## target
 
 TARGET_DIR="lib/classes"
 TARGET_JAR="$TARGET_DIR/Pure.jar"
 TARGET_SHASUM="$TARGET_DIR/Pure.shasum"
 
 function target_shasum()
 {
   shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null
 }
 
 function target_clean()
 {
   rm -rf "$TARGET_DIR"
 }
 
 [ -n "$FRESH" ] && target_clean
 
 
 ## build
 
 target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
 if [ "$?" -ne 0 ]; then
   echo "### Building Isabelle/Scala ..."
 
   target_clean
 
   BUILD_DIR="$TARGET_DIR/build"
   mkdir -p "$BUILD_DIR"
 
   (
     export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
     isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \
       -d "$BUILD_DIR" "${SOURCES[@]}"
   ) || fail "Failed to compile sources"
 
   CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
   mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")"
   echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE"
 
   cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/."
   cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/."
 
   isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \
     -C "$BUILD_DIR" META-INF \
     -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR"
 
   rm -rf "$BUILD_DIR"
 
   target_shasum > "$TARGET_SHASUM"
 fi
diff --git a/src/Tools/VSCode/src/preview_panel.scala b/src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala
+++ b/src/Tools/VSCode/src/preview_panel.scala
@@ -1,44 +1,44 @@
 /*  Title:      Tools/VSCode/src/preview_panel.scala
     Author:     Makarius
 
 HTML document preview.
 */
 
 package isabelle.vscode
 
 
 import isabelle._
 
 import java.io.{File => JFile}
 
 
 class Preview_Panel(resources: VSCode_Resources)
 {
   private val pending = Synchronized(Map.empty[JFile, Int])
 
   def request(file: JFile, column: Int): Unit =
     pending.change(map => map + (file -> column))
 
   def flush(channel: Channel): Boolean =
   {
     pending.change_result(map =>
     {
       val map1 =
         (map /: map.iterator)({ case (m, (file, column)) =>
           resources.get_model(file) match {
             case Some(model) =>
               val snapshot = model.snapshot()
               if (snapshot.is_outdated) m
               else {
-                val preview = Present.preview(resources, snapshot)
+                val preview = Presentation.preview(resources, snapshot)
                 channel.write(
                   Protocol.Preview_Response(file, column, preview.title, preview.content))
                 m - file
               }
             case None => m - file
           }
         })
       (map1.nonEmpty, map1)
     })
   }
 }
diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala
+++ b/src/Tools/jEdit/src/document_model.scala
@@ -1,695 +1,695 @@
 /*  Title:      Tools/jEdit/src/document_model.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Document model connected to jEdit buffer or external file: content of theory
 node or auxiliary file (blob).
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 import org.gjt.sp.jedit.{jEdit, View}
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
 
 
 object Document_Model
 {
   /* document models */
 
   sealed case class State(
     models: Map[Document.Node.Name, Document_Model] = Map.empty,
     buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
     overlays: Document.Overlays = Document.Overlays.empty)
   {
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
         (node_name, model) <- models.iterator
         if model.isInstanceOf[File_Model]
       } yield (node_name, model.asInstanceOf[File_Model])
 
     def document_blobs: Document.Blobs =
       Document.Blobs(
         (for {
           (node_name, model) <- models.iterator
           blob <- model.get_blob
         } yield (node_name -> blob)).toMap)
 
     def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
       : (Buffer_Model, State) =
     {
       val old_model =
         models.get(node_name) match {
           case Some(file_model: File_Model) => Some(file_model)
           case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
           case _ => None
         }
       val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
       (buffer_model,
         copy(models = models + (node_name -> buffer_model),
           buffer_models = buffer_models + (buffer -> buffer_model)))
     }
 
     def close_buffer(buffer: JEditBuffer): State =
     {
       buffer_models.get(buffer) match {
         case None => this
         case Some(buffer_model) =>
           val file_model = buffer_model.exit()
           copy(models = models + (file_model.node_name -> file_model),
             buffer_models = buffer_models - buffer)
       }
     }
 
     def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
       if (models.isDefinedAt(node_name)) this
       else {
         val edit = Text.Edit.insert(0, text)
         val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
         copy(models = models + (node_name -> model))
       }
   }
 
   private val state = Synchronized(State())  // owned by GUI thread
 
   def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
   def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
   def document_blobs(): Document.Blobs = state.value.document_blobs
 
 
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     Bibtex.entries_iterator(state.value.models)
 
   def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
       : Option[Completion.Result] =
     Bibtex.completion(history, rendering, caret, state.value.models)
 
 
   /* overlays */
 
   def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
     state.value.overlays(name)
 
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
     state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
 
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
     state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
 
 
   /* sync external files */
 
   def sync_files(changed_files: Set[JFile]): Boolean =
   {
     state.change_result(st =>
       {
         val changed_models =
           (for {
             (node_name, model) <- st.file_models_iterator
             file <- model.file if changed_files(file)
             text <- PIDE.resources.read_file_content(node_name)
             if model.content.text != text
           } yield {
             val content = Document_Model.File_Content(text)
             val edits = Text.Edit.replace(0, model.content.text, text)
             (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
           }).toList
         if (changed_models.isEmpty) (false, st)
         else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
       })
   }
 
 
   /* syntax */
 
   def syntax_changed(names: List[Document.Node.Name])
   {
     GUI_Thread.require {}
 
     val models = state.value.models
     for (name <- names.iterator; model <- models.get(name)) {
       model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
     }
   }
 
 
   /* init and exit */
 
   def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
   {
     GUI_Thread.require {}
     state.change_result(st =>
       st.buffer_models.get(buffer) match {
         case Some(buffer_model) if buffer_model.node_name == node_name =>
           buffer_model.init_token_marker
           (buffer_model, st)
         case _ =>
           val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
           buffer.propertiesChanged
           res
       })
   }
 
   def exit(buffer: Buffer)
   {
     GUI_Thread.require {}
     state.change(st =>
       if (st.buffer_models.isDefinedAt(buffer)) {
         val res = st.close_buffer(buffer)
         buffer.propertiesChanged
         res
       }
       else st)
   }
 
   def provide_files(session: Session, files: List[(Document.Node.Name, String)])
   {
     GUI_Thread.require {}
     state.change(st =>
       (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
   }
 
 
   /* required nodes */
 
   def required_nodes(): Set[Document.Node.Name] =
     (for {
       (node_name, model) <- state.value.models.iterator
       if model.node_required
     } yield node_name).toSet
 
   def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
   {
     GUI_Thread.require {}
 
     val changed =
       state.change_result(st =>
         st.models.get(name) match {
           case None => (false, st)
           case Some(model) =>
             val required = if (toggle) !model.node_required else set
             model match {
               case model1: File_Model if required != model1.node_required =>
                 (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
               case model1: Buffer_Model if required != model1.node_required =>
                 model1.set_node_required(required); (true, st)
               case _ => (false, st)
             }
         })
     if (changed) {
       PIDE.plugin.options_changed()
       PIDE.editor.flush()
     }
   }
 
   def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
     Document_Model.get(view.getBuffer).foreach(model =>
       node_required(model.node_name, toggle = toggle, set = set))
 
 
   /* flushed edits */
 
   def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
   {
     GUI_Thread.require {}
 
     state.change_result(st =>
       {
         val doc_blobs = st.document_blobs
 
         val buffer_edits =
           (for {
             (_, model) <- st.buffer_models.iterator
             edit <- model.flush_edits(doc_blobs, hidden).iterator
           } yield edit).toList
 
         val file_edits =
           (for {
             (node_name, model) <- st.file_models_iterator
             (edits, model1) <- model.flush_edits(doc_blobs, hidden)
           } yield (edits, node_name -> model1)).toList
 
         val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
 
         val purge_edits =
           if (purge) {
             val purged =
               (for ((node_name, model) <- st.file_models_iterator)
                yield (node_name -> model.purge_edits(doc_blobs))).toList
 
             val imports =
             {
               val open_nodes =
                 (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
               val touched_nodes = model_edits.map(_._1)
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
             val retain = PIDE.resources.dependencies(imports).theories.toSet
 
             for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
               yield edit
           }
           else Nil
 
         val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
         PIDE.plugin.file_watcher.purge(
           (for {
             (_, model) <- st1.file_models_iterator
             file <- model.file
           } yield file.getParentFile).toSet)
 
         ((doc_blobs, model_edits ::: purge_edits), st1)
       })
   }
 
 
   /* file content */
 
   sealed case class File_Content(text: String)
   {
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
   }
 
 
   /* HTTP preview */
 
   private val plain_text_prefix = "plain_text="
 
   def open_preview(view: View, plain_text: Boolean)
   {
     Document_Model.get(view.getBuffer) match {
       case Some(model) =>
         val name = model.node_name
         val url =
           PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
             (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
   }
 
   def http_handlers(http_root: String): List[HTTP.Handler] =
   {
     val fonts_root = http_root + "/fonts"
     val preview_root = http_root + "/preview"
 
     val preview =
       HTTP.get(preview_root, arg =>
         for {
           query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
           name = Library.perhaps_unprefix(plain_text_prefix, query)
           model <- get(PIDE.resources.node_name(name))
         }
         yield {
           val snapshot = model.await_stable_snapshot()
           val preview =
-            Present.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+            Presentation.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
               plain_text = query.startsWith(plain_text_prefix))
           HTTP.Response.html(preview.content)
         })
 
     List(HTTP.fonts(fonts_root), preview)
   }
 }
 
 sealed abstract class Document_Model extends Document.Model
 {
   /* perspective */
 
   def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
 
   def node_perspective(
     doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
   {
     GUI_Thread.require {}
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
 
       val reparse = snapshot.node.load_commands_changed(doc_blobs)
       val perspective =
         if (hidden) Text.Perspective.empty
         else {
           val view_ranges = document_view_ranges(snapshot)
           val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
           Text.Perspective(view_ranges ::: load_ranges)
         }
       val overlays = PIDE.editor.node_overlays(node_name)
 
       (reparse, Document.Node.Perspective(node_required, perspective, overlays))
     }
     else (false, Document.Node.no_perspective_text)
   }
 
 
   /* snapshot */
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       PIDE.options.seconds("editor_output_delay").sleep
       await_stable_snapshot()
     }
     else snapshot
   }
 }
 
 object File_Model
 {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
       false, Document.Node.no_perspective_text, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
     node_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     pending_edits: List[Text.Edit] = Nil): File_Model =
   {
     val file = JEdit_Lib.check_file(node_name.node)
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
     val node_required1 = node_required || File_Format.registry.is_theory(node_name)
     File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
   }
 }
 
 case class File_Model(
   session: Session,
   node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
   node_required: Boolean,
   last_perspective: Document.Node.Perspective_Text,
   pending_edits: List[Text.Edit]) extends Document_Model
 {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     range.try_substring(content.text)
 
 
   /* header */
 
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
       PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
 
   def node_position(offset: Text.Offset): Line.Node_Position =
     Line.Node_Position(node_name.node,
       Line.Position.zero.advance(content.text.substring(0, offset)))
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
     if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
 
 
   /* edits */
 
   def update_text(text: String): Option[File_Model] =
     Text.Edit.replace(0, content.text, text) match {
       case Nil => None
       case edits =>
         val content1 = Document_Model.File_Content(text)
         val pending_edits1 = pending_edits ::: edits
         Some(copy(content = content1, pending_edits = pending_edits1))
     }
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
     : Option[(List[Document.Edit_Text], File_Model)] =
   {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val edits = node_edits(node_header, pending_edits, perspective)
       Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
     }
     else None
   }
 
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
         !File_Format.registry.is_theory(node_name) &&
           (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))
       Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
     }
 
 
   /* snapshot */
 
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
   extends Document_Model
 {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     JEdit_Lib.get_text(buffer, range)
 
 
   /* header */
 
   def node_header(): Document.Node.Header =
   {
     GUI_Thread.require {}
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
         PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
       }
   }
 
 
   /* perspective */
 
   // owned by GUI thread
   private var _node_required = false
   def node_required: Boolean = _node_required
   def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
 
   def document_view_iterator: Iterator[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer)
       doc_view <- Document_View.get(text_area)
     } yield doc_view
 
   override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
   {
     GUI_Thread.require {}
 
     (for {
       doc_view <- document_view_iterator
       range <- doc_view.perspective(snapshot).ranges.iterator
     } yield range).toList
   }
 
 
   /* blob */
 
   // owned by GUI thread
   private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
 
   private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
 
   def get_blob: Option[Document.Blob] =
     GUI_Thread.require {
       if (is_theory) None
       else {
         val (bytes, text, chunk) =
           _blob match {
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.make_file_content(buffer)
               val text = buffer.getText(0, buffer.getLength)
               val chunk = Symbol.Text_Chunk(text)
               val x = (bytes, text, chunk)
               _blob = Some(x)
               x
           }
         val changed = pending_edits.nonEmpty
         Some(Document.Blob(bytes, text, chunk, changed))
       }
     }
 
 
   /* bibtex entries */
 
   // owned by GUI thread
   private var _bibtex_entries: Option[List[Text.Info[String]]] = None
 
   private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
       if (Bibtex.is_bibtex(node_name.node)) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>
             val text = JEdit_Lib.buffer_text(buffer)
             val entries =
               try { Bibtex.entries(text) }
               catch { case ERROR(msg) => Output.warning(msg); Nil }
             _bibtex_entries = Some(entries)
             entries
         }
       }
       else Nil
     }
 
 
   /* pending edits */
 
   private object pending_edits
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = Document.Node.no_perspective_text
 
     def nonEmpty: Boolean = synchronized { pending.nonEmpty }
     def get_edits: List[Text.Edit] = synchronized { pending.toList }
     def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
     def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
       synchronized { last_perspective = perspective }
 
     def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
       synchronized {
         GUI_Thread.require {}
 
         val edits = get_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
           pending.clear
           last_perspective = perspective
           node_edits(node_header(), edits, perspective)
         }
         else Nil
       }
 
     def edit(edits: List[Text.Edit]): Unit = synchronized
     {
       GUI_Thread.require {}
 
       reset_blob()
       reset_bibtex_entries()
 
       for (doc_view <- document_view_iterator)
         doc_view.rich_text_area.active_reset()
 
       pending ++= edits
       PIDE.editor.invoke()
     }
   }
 
   def is_stable: Boolean = !pending_edits.nonEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     pending_edits.flush_edits(doc_blobs, hidden)
 
 
   /* buffer listener */
 
   private val buffer_listener: BufferListener = new BufferAdapter
   {
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int)
     {
       pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
     {
       pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
     }
   }
 
 
   /* syntax */
 
   def syntax_changed()
   {
     JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
     for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
       Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
         invoke(text_area)
     buffer.invalidateCachedFoldLevels
   }
 
   def init_token_marker()
   {
     Isabelle.buffer_token_marker(buffer) match {
       case Some(marker) if marker != buffer.getTokenMarker =>
         buffer.setTokenMarker(marker)
         syntax_changed()
       case _ =>
     }
   }
 
 
   /* init */
 
   def init(old_model: Option[File_Model]): Buffer_Model =
   {
     GUI_Thread.require {}
 
     old_model match {
       case None =>
         pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
         set_node_required(file_model.node_required)
         pending_edits.set_last_perspective(file_model.last_perspective)
         pending_edits.edit(
           file_model.pending_edits :::
             Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
     }
 
     buffer.addBufferListener(buffer_listener)
     init_token_marker()
 
     this
   }
 
 
   /* exit */
 
   def exit(): File_Model =
   {
     GUI_Thread.require {}
 
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
     File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
       pending_edits.get_last_perspective, pending_edits.get_edits)
   }
 }