diff --git a/src/Pure/Admin/build_postgresql.scala b/src/Pure/Admin/build_postgresql.scala
--- a/src/Pure/Admin/build_postgresql.scala
+++ b/src/Pure/Admin/build_postgresql.scala
@@ -1,125 +1,125 @@
 /*  Title:      Pure/Admin/build_postgresql.scala
     Author:     Makarius
 
 Build Isabelle postgresql component from official download.
 */
 
 package isabelle
 
 
 object Build_PostgreSQL {
   /* URLs */
 
   val notable_urls =
     List("https://jdbc.postgresql.org", "https://jdbc.postgresql.org/download.html")
 
   val default_download_url = "https://jdbc.postgresql.org/download/postgresql-42.5.0.jar"
 
 
   /* build postgresql */
 
   def build_postgresql(
     download_url: String = default_download_url,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
     /* name and version */
 
     def err(): Nothing = error("Malformed jar download URL: " + quote(download_url))
 
     val Name = """^.*/([^/]+)\.jar""".r
     val download_name = download_url match { case Name(name) => name case _ => err() }
  
     val Version = """^.[^0-9]*([0-9].*)$""".r
     val download_version = download_name match { case Version(version) => version case _ => err() }
 
 
     /* component */
 
     val component_dir =
       Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
 
 
     /* LICENSE */
 
     File.write(component_dir.LICENSE,
 """Copyright (c) 1997, PostgreSQL Global Development Group
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
 
 1. Redistributions of source code must retain the above copyright notice,
    this list of conditions and the following disclaimer.
 2. Redistributions in binary form must reproduce the above copyright notice,
    this list of conditions and the following disclaimer in the documentation
    and/or other materials provided with the distribution.
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
 LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 POSSIBILITY OF SUCH DAMAGE.
 """)
 
 
     /* README */
 
     File.write(component_dir.README,
 """This is PostgreSQL JDBC """ + download_version + """ from
 """ + notable_urls.mkString(" and ") + """
 
         Makarius
         """ + Date.Format.date(Date.now()) + "\n")
 
 
     /* settings */
 
     component_dir.write_settings("""
 classpath "$COMPONENT/""" + download_name + """.jar"
 """)
 
 
     /* jar */
 
-    val jar = component_dir.path + Path.basic(download_name).ext("jar")
+    val jar = component_dir.path + Path.basic(download_name).jar
     Isabelle_System.download_file(download_url, jar, progress = progress)
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_postgresql", "build Isabelle postgresql component from official download",
       Scala_Project.here,
       { args =>
         var target_dir = Path.current
         var download_url = default_download_url
 
         val getopts = Getopts("""
 Usage: isabelle build_postgresql [OPTIONS]
 
   Options are:
     -D DIR       target directory (default ".")
     -U URL       download URL
                  (default: """" + default_download_url + """")
 
   Build postgresql component from the specified download URL (JAR), see also
   """ + notable_urls.mkString(" and "),
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "U:" -> (arg => download_url = arg))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress()
 
         build_postgresql(download_url, progress = progress, target_dir = target_dir)
       })
 }
diff --git a/src/Pure/Admin/build_sqlite.scala b/src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala
+++ b/src/Pure/Admin/build_sqlite.scala
@@ -1,111 +1,111 @@
 /*  Title:      Pure/Admin/build_sqlite.scala
     Author:     Makarius
 
 Build Isabelle sqlite-jdbc component from official download.
 */
 
 package isabelle
 
 
 object Build_SQLite {
   /* build sqlite */
 
   val default_download_url =
     "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.39.4.1/sqlite-jdbc-3.39.4.1.jar"
 
   def build_sqlite(
     download_url: String = default_download_url,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
     val Download_Name = """^.*/([^/]+)\.jar""".r
     val download_name =
       download_url match {
         case Download_Name(download_name) => download_name
         case _ => error("Malformed jar download URL: " + quote(download_url))
       }
 
 
     /* component */
 
     val component_dir =
       Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
 
 
     /* README */
 
     File.write(component_dir.README,
       "This is " + download_name + " from\n" + download_url +
         "\n\n        Makarius\n        " + Date.Format.date(Date.now()) + "\n")
 
 
     /* settings */
 
     component_dir.write_settings("""
 ISABELLE_SQLITE_HOME="$COMPONENT"
 
 classpath "$ISABELLE_SQLITE_HOME/lib/""" + download_name + """.jar"
 """)
 
 
     /* jar */
 
-    val jar = component_dir.lib + Path.basic(download_name).ext("jar")
+    val jar = component_dir.lib + Path.basic(download_name).jar
     Isabelle_System.make_directory(jar.dir)
     Isabelle_System.download_file(download_url, jar, progress = progress)
 
     Isabelle_System.with_tmp_dir("build") { jar_dir =>
       Isabelle_System.extract(jar, jar_dir)
 
       val jar_files =
         List(
           "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE" -> ".",
           "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".",
           "org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux",
           "org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux",
           "org/sqlite/native/Mac/aarch64/libsqlitejdbc.jnilib" -> "arm64-darwin",
           "org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin",
           "org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows")
 
       for ((file, dir) <- jar_files) {
         val target = Isabelle_System.make_directory(component_dir.path + Path.explode(dir))
         Isabelle_System.copy_file(jar_dir + Path.explode(file), target)
       }
 
       File.set_executable(component_dir.path + Path.explode("x86_64-windows/sqlitejdbc.dll"), true)
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_sqlite", "build Isabelle sqlite-jdbc component from official download",
       Scala_Project.here,
       { args =>
         var target_dir = Path.current
         var download_url = default_download_url
 
         val getopts = Getopts("""
 Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
 
   Options are:
     -D DIR       target directory (default ".")
     -U URL       download URL
                  (default: """" + default_download_url + """")
 
   Build sqlite-jdbc component from the specified download URL (JAR), see also
   https://github.com/xerial/sqlite-jdbc and
   https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "U:" -> (arg => download_url = arg))
 
         val more_args = getopts(args)
         if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress()
 
         build_sqlite(download_url = download_url, progress = progress, target_dir = target_dir)
       })
 }
diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala
--- a/src/Pure/General/path.scala
+++ b/src/Pure/General/path.scala
@@ -1,314 +1,318 @@
 /*  Title:      Pure/General/path.scala
     Author:     Makarius
 
 Algebra of file-system paths: basic POSIX notation, extended by named
 roots (e.g. //foo) and variables (e.g. $BAR).
 */
 
 package isabelle
 
 
 import java.util.{Map => JMap}
 import java.io.{File => JFile}
 import java.nio.file.{Path => JPath}
 
 import scala.util.matching.Regex
 
 
 object Path {
   /* path elements */
 
   sealed abstract class Elem
   private case class Root(name: String) extends Elem
   private case class Basic(name: String) extends Elem
   private case class Variable(name: String) extends Elem
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
     error(msg + " path element " + quote(s))
 
   private val illegal_elem = Set("", "~", "~~", ".", "..")
   private val illegal_char = "/\\$:\"'<>|?*"
 
   private def check_elem(s: String): String =
     if (illegal_elem.contains(s)) err_elem("Illegal", s)
     else {
       for (c <- s) {
         if (c.toInt < 32)
           err_elem("Illegal control character " + c.toInt + " in", s)
         if (illegal_char.contains(c))
           err_elem("Illegal character " + quote(c.toString) + " in", s)
       }
       s
     }
 
   private def root_elem(s: String): Elem = Root(check_elem(s))
   private def basic_elem(s: String): Elem = Basic(check_elem(s))
   private def variable_elem(s: String): Elem = Variable(check_elem(s))
 
   private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
     (y, xs) match {
       case (Root(_), _) => List(y)
       case (Parent, Root(_) :: _) => xs
       case (Parent, Basic(_) :: rest) => rest
       case _ => y :: xs
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
     elems.foldRight(List.empty[Elem])(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
       case Root("") => ""
       case Root(s) => "//" + s
       case Basic(s) => s
       case Variable("USER_HOME") if short => "~"
       case Variable("ISABELLE_HOME") if short => "~~"
       case Variable(s) => "$" + s
       case Parent => ".."
     }
 
   private def squash_elem(elem: Elem): String =
     elem match {
       case Root("") => "ROOT"
       case Root(s) => "SERVER_" + s
       case Basic(s) => s
       case Variable(s) => s
       case Parent => "PARENT"
     }
 
 
   /* path constructors */
 
   val current: Path = new Path(Nil)
   val root: Path = new Path(List(Root("")))
   def named_root(s: String): Path = new Path(List(root_elem(s)))
   def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem))
   def basic(s: String): Path = new Path(List(basic_elem(s)))
   def variable(s: String): Path = new Path(List(variable_elem(s)))
   val parent: Path = new Path(List(Parent))
 
   val USER_HOME: Path = variable("USER_HOME")
   val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
 
   val index_html: Path = basic("index.html")
 
 
   /* explode */
 
   def explode(str: String): Path = {
     def explode_elem(s: String): Elem =
       try {
         if (s == "..") Parent
         else if (s == "~") Variable("USER_HOME")
         else if (s == "~~") Variable("ISABELLE_HOME")
         else if (s.startsWith("$")) variable_elem(s.substring(1))
         else basic_elem(s)
       }
       catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
   
     val ss = space_explode('/', str)
     val r = ss.takeWhile(_.isEmpty).length
     val es = ss.dropWhile(_.isEmpty)
     val (roots, raw_elems) =
       if (r == 0) (Nil, es)
       else if (r == 1) (List(Root("")), es)
       else if (es.isEmpty) (List(Root("")), Nil)
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
     new Path(norm_elems(elems reverse_::: roots))
   }
 
   def is_wellformed(str: String): Boolean =
     try { explode(str); true } catch { case ERROR(_) => false }
 
   def is_valid(str: String): Boolean =
     try { explode(str).expand; true } catch { case ERROR(_) => false }
 
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
 
 
   /* encode */
 
   val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
 
 
   /* reserved names */
 
   private val reserved_windows: Set[String] =
     Set("CON", "PRN", "AUX", "NUL",
       "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
       "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9")
 
   def is_reserved(name: String): Boolean =
     Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
 
 
   /* case-insensitive names */
 
   def check_case_insensitive(paths: List[Path]): Unit = {
     val table =
       paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
         val name = path.expand.implode
         tab.insert(Word.lowercase(name), name)
       }
     val collisions =
       (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
     if (collisions.nonEmpty) {
       error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n  "))
     }
   }
 
   def eq_case_insensitive(path1: Path, path2: Path): Boolean =
     path1 == path2 ||
     Word.lowercase(path1.expand.implode) == Word.lowercase(path2.expand.implode)
 }
 
 
 final class Path private(
   protected val elems: List[Path.Elem]  // reversed elements
 ) {
   override def hashCode: Int = elems.hashCode
   override def equals(that: Any): Boolean =
     that match {
       case other: Path => elems == other.elems
       case _ => false
     }
 
   def is_current: Boolean = elems.isEmpty
   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
   def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
   def all_basic: Boolean = elems.forall(_.isInstanceOf[Path.Basic])
   def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
 
   def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
 
 
   /* implode */
 
   private def gen_implode(short: Boolean): String =
     elems match {
       case Nil => "."
       case List(Path.Root("")) => "/"
       case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/")
     }
   def implode: String = gen_implode(false)
   def implode_short: String = gen_implode(true)
 
   override def toString: String = quote(implode)
 
 
   /* base element */
 
   private def split_path: (Path, String) =
     elems match {
       case Path.Basic(s) :: xs => (new Path(xs), s)
       case _ => error("Cannot split path into dir/base: " + toString)
     }
 
   def dir: Path = split_path._1
   def base: Path = new Path(List(Path.Basic(split_path._2)))
 
   def ends_with(a: String): Boolean =
     elems match {
       case Path.Basic(b) :: _ => b.endsWith(a)
       case _ => false
     }
   def is_java: Boolean = ends_with(".java")
   def is_scala: Boolean = ends_with(".scala")
   def is_pdf: Boolean = ends_with(".pdf")
   def is_latex: Boolean =
     ends_with(".tex") ||
     ends_with(".sty") ||
     ends_with(".cls") ||
     ends_with(".clo")
 
   def ext(e: String): Path =
     if (e == "") this
     else {
       val (prfx, s) = split_path
       prfx + Path.basic(s + "." + e)
     }
 
+  def bib: Path = ext("bib")
+  def blg: Path = ext("blg")
+  def db: Path = ext("db")
   def gz: Path = ext("gz")
   def html: Path = ext("html")
+  def jar: Path = ext("jar")
   def log: Path = ext("log")
   def orig: Path = ext("orig")
   def patch: Path = ext("patch")
   def pdf: Path = ext("pdf")
   def shasum: Path = ext("shasum")
   def tar: Path = ext("tar")
   def tex: Path = ext("tex")
   def thy: Path = ext("thy")
   def xml: Path = ext("xml")
   def xz: Path = ext("xz")
   def zst: Path = ext("zst")
 
   def backup: Path = {
     val (prfx, s) = split_path
     prfx + Path.basic(s + "~")
   }
 
   def backup2: Path = {
     val (prfx, s) = split_path
     prfx + Path.basic(s + "~~")
   }
 
   def exe: Path = ext("exe")
   def exe_if(b: Boolean): Path = if (b) exe else this
   def platform_exe: Path = exe_if(Platform.is_windows)
 
   private val Ext = new Regex("(.*)\\.([^.]*)")
 
   def split_ext: (Path, String) = {
     val (prefix, base) = split_path
     base match {
       case Ext(b, e) => (prefix + Path.basic(b), e)
       case _ => (prefix + Path.basic(base), "")
     }
   }
 
   def drop_ext: Path = split_ext._1
   def get_ext: String = split_ext._2
 
   def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem))))
 
 
   /* expand */
 
   def expand_env(env: JMap[String, String]): Path = {
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
           val path = Path.explode(Isabelle_System.getenv_strict(s, env))
           if (path.elems.exists(_.isInstanceOf[Path.Variable]))
             error("Illegal path variable nesting: " + Properties.Eq(s, path.toString))
           else path.elems
         case x => List(x)
       }
 
     new Path(Path.norm_elems(elems.flatMap(eval)))
   }
 
   def expand: Path = expand_env(Isabelle_System.settings())
 
   def file_name: String = expand.base.implode
 
 
   /* platform files */
 
   def file: JFile = File.platform_file(this)
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
   def java_path: JPath = file.toPath
 
   def absolute_file: JFile = File.absolute(file)
   def canonical_file: JFile = File.canonical(file)
 
   def absolute: Path = File.path(absolute_file)
   def canonical: Path = File.path(canonical_file)
 }
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,855 +1,855 @@
 /*  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
 import scala.util.matching.Regex
 
 import isabelle.{Token => Isar_Token}
 
 
 object Bibtex {
   /** file format **/
 
   class File_Format extends isabelle.File_Format {
     val format_name: String = "bibtex"
     val file_ext: String = "bib"
 
     override def parse_data(name: String, text: String): Bibtex.Entries =
       Bibtex.Entries.parse(text, Isar_Token.Pos.file(name))
 
     override def theory_suffix: String = "bibtex_file"
     override def theory_content(name: String): String =
       """theory "bib" imports Pure begin bibtex_file "." end"""
     override def theory_excluded(name: String): Boolean = name == "bib"
 
     override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
       val name = snapshot.node_name
       if (detect(name.node)) {
         val title = "Bibliography " + quote(snapshot.node_name.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(Browser_Info.HTML_Document(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")
+    val log_path = dir + Path.explode(root_name).blg
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
       val Error2 = """^(I found no .+)$""".r
       val Error3 = """^(.+)---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) => Some("Bibtex error: " + msg)
           case Error3(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): Unit = {
       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_String("bibtex_check_database") {
     val here = Scala_Project.here
     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 */
 
   sealed case class Entry(name: String, pos: Position.T) {
     def encode: String = YXML.string_of_body(XML.Encode.properties(Markup.Name(name) ::: pos))
   }
 
   object Entries {
     val empty: Entries = apply(Nil)
 
     def apply(entries: List[Entry], errors: List[String] = Nil): Entries =
       new Entries(entries, errors)
 
     def parse(text: String, start: Isar_Token.Pos = Isar_Token.Pos.start): Entries = {
       val entries = new mutable.ListBuffer[Entry]
       var pos = start
       var err_line = 0
 
       try {
         for (chunk <- Bibtex.parse(text)) {
           val pos1 = pos.advance(chunk.source)
           if (chunk.name != "" && !chunk.is_command) {
             entries += Entry(chunk.name, pos.position(pos1.offset))
           }
           if (chunk.is_malformed && err_line == 0) { err_line = pos.line }
           pos = pos1
         }
 
         val err_pos =
           if (err_line == 0 || pos.file.isEmpty) Position.none
           else Position.Line_File(err_line, pos.file)
         val errors =
           if (err_line == 0) Nil
           else List("Malformed bibtex file" + Position.here(err_pos))
 
         apply(entries.toList, errors = errors)
       }
       catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
     }
   }
 
   final class Entries private(val entries: List[Entry], val errors: List[String]) {
     override def toString: String = "Bibtex.Entries(" + entries.length + ")"
 
     def ::: (other: Entries): Entries =
       new Entries(entries ::: other.entries, errors ::: other.errors)
   }
 
   object Session_Entries extends Scala.Fun("bibtex_session_entries") {
     val here = Scala_Project.here
 
     override def invoke(session: Session, args: List[Bytes]): List[Bytes] = {
       val sessions = session.resources.sessions_structure
       val id = Value.Long.parse(Library.the_single(args).text)
       val qualifier =
         session.get_state().lookup_id(id) match {
           case None => Sessions.DRAFT
           case Some(st) => sessions.theory_qualifier(st.command.node_name.theory)
         }
       val res =
         if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil
         else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.encode)
       res.map(Bytes.apply)
     }
   }
 
 
 
   /** 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_Type(
     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_Type] =
     List(
       Entry_Type("Article",
         List("author", "title"),
         List("journal", "year"),
         List("volume", "number", "pages", "month", "note")),
       Entry_Type("InProceedings",
         List("author", "title"),
         List("booktitle", "year"),
         List("editor", "volume", "number", "series", "pages", "month", "address",
           "organization", "publisher", "note")),
       Entry_Type("InCollection",
         List("author", "title", "booktitle"),
         List("publisher", "year"),
         List("editor", "volume", "number", "series", "type", "chapter", "pages",
           "edition", "month", "address", "note")),
       Entry_Type("InBook",
         List("author", "editor", "title", "chapter"),
         List("publisher", "year"),
         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
       Entry_Type("Proceedings",
         List("title", "year"),
         List(),
         List("booktitle", "editor", "volume", "number", "series", "address", "month",
           "organization", "publisher", "note")),
       Entry_Type("Book",
         List("author", "editor", "title"),
         List("publisher", "year"),
         List("volume", "number", "series", "address", "edition", "month", "note")),
       Entry_Type("Booklet",
         List("title"),
         List(),
         List("author", "howpublished", "address", "month", "year", "note")),
       Entry_Type("PhdThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry_Type("MastersThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry_Type("TechReport",
         List("author", "title", "institution", "year"),
         List(),
         List("type", "number", "address", "month", "note")),
       Entry_Type("Manual",
         List("title"),
         List(),
         List("author", "organization", "address", "edition", "month", "year", "note")),
       Entry_Type("Unpublished",
         List("author", "title", "note"),
         List(),
         List("month", "year")),
       Entry_Type("Misc",
         List(),
         List(),
         List("author", "title", "howpublished", "month", "year", "note")))
 
   def known_entry(kind: String): Option[Entry_Type] =
     known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
 
 
 
   /** 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: String = 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 {
         tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
       }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
     def is_entry: Boolean = Bibtex.known_entry(kind).isDefined && 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 = 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,
           "bad delimiter depth")
 
         def apply(in: Input): ParseResult[(String, Delimited)] = {
           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: Parser[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 (known_entry(a).isDefined) 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) {
       val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
       (result : @unchecked) 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) {
-        Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
+        Isabelle_System.copy_file(a.bib, tmp_dir + Path.basic(b).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)) + ")")
         }
       Isabelle_System.copy_file(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
     }
   }
 
 
 
   /** cite commands and antiquotations **/
 
   /* cite commands */
 
   def cite_commands(options: Options): List[String] =
     Library.space_explode(',', options.string("document_cite_commands"))
 
   val CITE = "cite"
   val NOCITE = "nocite"
 
 
   /* citations within theory source */
 
   object Cite {
     def unapply(tree: XML.Tree): Option[Inner] =
       tree match {
         case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
           val kind = Markup.Kind.unapply(props).getOrElse(CITE)
           val citations = Markup.Citations.get(props)
           val pos = props.filter(Markup.position_property)
           Some(Inner(kind, citations, body, pos))
         case _ => None
       }
 
     sealed case class Inner(kind: String, citations: String, location: XML.Body, pos: Position.T) {
       def nocite: Inner = copy(kind = NOCITE, location = Nil)
 
       def latex_text: Latex.Text = {
         val props =
           (if (kind.nonEmpty) Markup.Kind(kind) else Nil) :::
           Markup.Citations(citations) ::: pos
         List(XML.Elem(Markup.Latex_Cite(props), location))
       }
 
       override def toString: String = citations
     }
 
     sealed case class Outer(kind: String, body: String, start: Isar_Token.Pos) {
       def pos: Position.T = start.position()
 
       def parse: Option[Inner] = {
         val tokens = Isar_Token.explode(Parsers.keywords, body)
         Parsers.parse_all(Parsers.inner(pos), Isar_Token.reader(tokens, start)) match {
           case Parsers.Success(res, _) => Some(res)
           case _ => None
         }
       }
 
       def errors: List[String] =
         if (parse.isDefined) Nil
         else List("Malformed citation" + Position.here(pos))
 
       override def toString: String =
         parse match {
           case Some(inner) => inner.toString
           case None => "<malformed>"
         }
     }
 
     object Parsers extends Parse.Parsers {
       val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "using"
 
       val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("")
       val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(","))
       val kind: Parser[String] = $$$("using") ~! name ^^ { case _ ~ x => x } | success(CITE)
 
       def inner(pos: Position.T): Parser[Inner] =
         location ~ citations ~ kind ^^
           { case x ~ y ~ z => Inner(z, y, XML.string(x), pos) }
     }
 
     def parse(
       cite_commands: List[String],
       text: String,
       start: Isar_Token.Pos = Isar_Token.Pos.start
     ): List[Outer] = {
       val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix)
       val special = (controls ::: controls.map(Symbol.decode)).toSet
 
       val Parsers = Antiquote.Parsers
       Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match {
         case Parsers.Success(ants, _) =>
           var pos = start
           val result = new mutable.ListBuffer[Outer]
           for (ant <- ants) {
             ant match {
               case Antiquote.Control(source) =>
                 for {
                   head <- Symbol.iterator(source).nextOption
                   kind <- Symbol.control_name(Symbol.encode(head))
                 } {
                   val rest = source.substring(head.length)
                   val (body, pos1) =
                     if (rest.isEmpty) (rest, pos)
                     else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open))
                   result += Outer(kind, body, pos1)
                 }
               case _ =>
             }
             pos = pos.advance(ant.source)
           }
           result.toList
         case _ => error("Unexpected failure parsing special antiquotations:\n" + text)
       }
     }
   }
 
 
   /* update old forms: @{cite ...} and \cite{...} */
 
   def cite_antiquotation(name: String, body: String): String =
     """\<^""" + name + """>\<open>""" + body + """\<close>"""
 
   def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
     val body =
       (if (location.isEmpty) "" else Symbol.cartouche(location) + " in ") +
       citations.map(quote).mkString(" and ")
     cite_antiquotation(name, body)
   }
 
   private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r
   private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r
 
   def update_cite_commands(str: String): String =
     Cite_Command.replaceAllIn(str, { m =>
       val name = m.group(1)
       val loc = m.group(2)
       val location =
         if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
         else loc
       val citations = Library.space_explode(',', m.group(3)).map(_.trim)
       Regex.quoteReplacement(cite_antiquotation(name, location, citations))
     })
 
   def update_cite_antiquotation(cite_commands: List[String], str: String): String = {
     val opt_body =
       for {
         str1 <- Library.try_unprefix("@{cite", str)
         str2 <- Library.try_unsuffix("}", str1)
       } yield str2.trim
 
     opt_body match {
       case None => str
       case Some(body0) =>
         val (name, body1) =
           Cite_Macro.findFirstMatchIn(body0) match {
             case None => (CITE, body0)
             case Some(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, ""))
           }
         val body2 = body1.replace("""\<close>""", """\<close> in""")
         if (cite_commands.contains(name)) cite_antiquotation(name, body2)
         else cite_antiquotation(CITE, body2 + " using " + quote(name))
     }
   }
 }
diff --git a/src/Pure/Thy/latex.scala b/src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala
+++ b/src/Pure/Thy/latex.scala
@@ -1,472 +1,472 @@
 /*  Title:      Pure/Thy/latex.scala
     Author:     Makarius
 
 Support for LaTeX.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.TreeMap
 import scala.util.matching.Regex
 
 
 object Latex {
   /* output name for LaTeX macros */
 
   private val output_name_map: Map[Char, String] =
     Map('_' -> "UNDERSCORE",
       '\'' -> "PRIME",
       '0' -> "ZERO",
       '1' -> "ONE",
       '2' -> "TWO",
       '3' -> "THREE",
       '4' -> "FOUR",
       '5' -> "FIVE",
       '6' -> "SIX",
       '7' -> "SEVEN",
       '8' -> "EIGHT",
       '9' -> "NINE")
 
   def output_name(name: String): String =
     if (name.exists(output_name_map.keySet)) {
       val res = new StringBuilder
       for (c <- name) {
         output_name_map.get(c) match {
           case None => res += c
           case Some(s) => res ++= s
         }
       }
       res.toString
     }
     else name
 
 
   /* index entries */
 
   def index_escape(str: String): String = {
     val special1 = "!\"@|"
     val special2 = "\\{}#"
     if (str.exists(c => special1.contains(c) || special2.contains(c))) {
       val res = new StringBuilder
       for (c <- str) {
         if (special1.contains(c)) {
           res ++= "\\char"
           res ++= Value.Int(c)
         }
         else {
           if (special2.contains(c)) { res += '"'}
           res += c
         }
       }
       res.toString
     }
     else str
   }
 
   object Index_Item {
     sealed case class Value(text: Text, like: String)
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Wrapped_Elem(Markup.Latex_Index_Item(_), text, like) =>
           Some(Value(text, XML.content(like)))
         case _ => None
       }
   }
 
   object Index_Entry {
     sealed case class Value(items: List[Index_Item.Value], kind: String)
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Elem(Markup.Latex_Index_Entry(kind), body) =>
           val items = body.map(Index_Item.unapply)
           if (items.forall(_.isDefined)) Some(Value(items.map(_.get), kind)) else None
         case _ => None
       }
   }
 
 
   /* tags */
 
   object Tags {
     object Op extends Enumeration {
       val fold, drop, keep = Value
     }
 
     val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
 
     private def explode(spec: String): List[String] =
       Library.space_explode(',', spec)
 
     def apply(spec: String): Tags =
       new Tags(spec,
         (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) {
           case (m, tag) =>
             tag.toList match {
               case '/' :: cs => m + (cs.mkString -> Op.fold)
               case '-' :: cs => m + (cs.mkString -> Op.drop)
               case '+' :: cs => m + (cs.mkString -> Op.keep)
               case cs => m + (cs.mkString -> Op.keep)
             }
         })
 
     val empty: Tags = apply("")
   }
 
   class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value]) {
     override def toString: String = spec
 
     def get(name: String): Option[Tags.Op.Value] = map.get(name)
 
     def sty(comment_latex: Boolean): File.Content = {
       val path = Path.explode("isabelletags.sty")
       val comment =
         if (comment_latex) """\usepackage{comment}"""
         else """%plain TeX version of comment package -- much faster!
 \let\isafmtname\fmtname\def\fmtname{plain}
 \usepackage{comment}
 \let\fmtname\isafmtname"""
       val tags =
         (for ((name, op) <- map.iterator)
           yield "\\isa" + op + "tag{" + name + "}").toList
       File.content(path, comment + """
 
 \newcommand{\isakeeptag}[1]%
 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
 \newcommand{\isadroptag}[1]%
 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
 \newcommand{\isafoldtag}[1]%
 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
 
 """ + Library.terminate_lines(tags))
     }
   }
 
 
   /* output text and positions */
 
   type Text = XML.Body
 
   def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n"
 
   def init_position(file_pos: String): List[String] =
     if (file_pos.isEmpty) Nil
     else List("\\endinput\n", position(Markup.FILE, file_pos))
 
   def append_position(path: Path, file_pos: String): Unit = {
     val pos = init_position(file_pos).mkString
     if (pos.nonEmpty) {
       val sep = if (File.read(path).endsWith("\n")) "" else "\n"
       File.append(path, sep + pos)
     }
   }
 
   def copy_file(src: Path, dst: Path): Unit = {
     Isabelle_System.copy_file(src, dst)
     if (src.is_latex) {
       val target = if (dst.is_dir) dst + src.base else dst
       val file_pos = File.symbolic_path(src)
       append_position(target, file_pos)
     }
   }
 
   def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
     Isabelle_System.copy_file_base(base_dir, src, target_dir)
     if (src.is_latex) {
       val file_pos = File.symbolic_path(base_dir + src)
       append_position(target_dir + src, file_pos)
     }
   }
 
   class Output(val options: Options) {
     def latex_output(latex_text: Text): String = make(latex_text)
 
     def latex_macro0(name: String, optional_argument: String = ""): Text =
       XML.string("\\" + name + optional_argument)
 
     def latex_macro(name: String, body: Text, optional_argument: String = ""): Text =
       XML.enclose("\\" + name + optional_argument + "{", "}", body)
 
     def latex_environment(name: String, body: Text, optional_argument: String = ""): Text =
       XML.enclose(
         "%\n\\begin{" + name + "}" + optional_argument + "%\n",
         "%\n\\end{" + name + "}", body)
 
     def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text =
       XML.enclose(
         "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{",
         "%\n}\n", body)
 
     def latex_body(kind: String, body: Text, optional_argument: String = ""): Text =
       latex_environment("isamarkup" + kind, body, optional_argument)
 
     def latex_tag(name: String, body: Text, delim: Boolean = false): Text = {
       val s = output_name(name)
       val kind = if (delim) "delim" else "tag"
       val end = if (delim) "" else "{\\isafold" + s + "}%\n"
       if (options.bool("document_comment_latex")) {
         XML.enclose(
           "%\n\\begin{isa" + kind + s + "}\n",
           "%\n\\end{isa" + kind + s + "}\n" + end, body)
       }
       else {
         XML.enclose(
           "%\n\\isa" + kind + s + "\n",
           "%\n\\endisa" + kind + s + "\n" + end, body)
       }
     }
 
     def cite(inner: Bibtex.Cite.Inner): Text = {
       val body =
         latex_macro0(inner.kind) :::
         (if (inner.location.isEmpty) Nil
          else XML.string("[") ::: inner.location ::: XML.string("]")) :::
         XML.string("{" + inner.citations + "}")
 
       if (inner.pos.isEmpty) body
       else List(XML.Elem(Markup.Latex_Output(inner.pos), body))
     }
 
     def index_item(item: Index_Item.Value): String = {
       val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
       val text = index_escape(latex_output(item.text))
       like + text
     }
 
     def index_entry(entry: Index_Entry.Value): Text = {
       val items = entry.items.map(index_item).mkString("!")
       val kind = if (entry.kind.isEmpty) "" else "|" + index_escape(entry.kind)
       latex_macro("index", XML.string(items + kind))
     }
 
 
     /* standard output of text with per-line positions */
 
     def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body =
       error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
         ":\n" + XML.string_of_tree(elem))
 
     def make(
       latex_text: Text,
       file_pos: String = "",
       line_pos: Properties.T => Option[Int] = Position.Line.unapply
     ): String = {
       var line = 1
       val result = new mutable.ListBuffer[String]
       val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
 
       val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos)
 
       def traverse(xml: XML.Body): Unit = {
         xml.foreach {
           case XML.Text(s) =>
             line += Library.count_newlines(s)
             result += s
           case elem @ XML.Elem(markup, body) =>
             val a = Markup.Optional_Argument.get(markup.properties)
             traverse {
               markup match {
                 case Markup.Document_Latex(props) =>
                   if (positions.nonEmpty) {
                     for (l <- line_pos(props)) {
                       val s = position(Value.Int(line), Value.Int(l))
                       if (positions.last != s) positions += s
                     }
                   }
                   body
                 case Markup.Latex_Output(_) => XML.string(latex_output(body))
                 case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a)
                 case Markup.Latex_Macro(name) => latex_macro(name, body, a)
                 case Markup.Latex_Environment(name) => latex_environment(name, body, a)
                 case Markup.Latex_Heading(kind) => latex_heading(kind, body, a)
                 case Markup.Latex_Body(kind) => latex_body(kind, body, a)
                 case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true)
                 case Markup.Latex_Tag(name) => latex_tag(name, body)
                 case Markup.Latex_Cite(_) =>
                   elem match {
                     case Bibtex.Cite(inner) => cite(inner)
                     case _ => unknown_elem(elem, file_position)
                   }
                 case Markup.Latex_Index_Entry(_) =>
                   elem match {
                     case Index_Entry(entry) => index_entry(entry)
                     case _ => unknown_elem(elem, file_position)
                   }
                 case _ => unknown_elem(elem, file_position)
               }
             }
         }
       }
       traverse(latex_text)
 
       result ++= positions
       result.mkString
     }
   }
 
 
   /* generated .tex file */
 
   private val File_Pattern = """^%:%file=(.+)%:%$""".r
   private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
 
   def read_tex_file(tex_file: Path): Tex_File = {
     val positions =
       Line.logical_lines(File.read(tex_file)).reverse.
         takeWhile(_ != "\\endinput").reverse
 
     val source_file =
       positions match {
         case File_Pattern(file) :: _ => Some(file)
         case _ => None
       }
 
     val source_lines =
       if (source_file.isEmpty) Nil
       else
         positions.flatMap(line =>
           line match {
             case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
             case _ => None
           })
 
     new Tex_File(tex_file, source_file, source_lines)
   }
 
   final class Tex_File private[Latex](
     tex_file: Path,
     source_file: Option[String],
     source_lines: List[(Int, Int)]
   ) {
     override def toString: String = tex_file.toString
 
     def source_position(l: Int): Option[Position.T] =
       source_file match {
         case None => None
         case Some(file) =>
           val source_line =
             source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
               foldLeft(0) { case (_, (_, n)) => n }
           if (source_line == 0) None else Some(Position.Line_File(source_line, file))
       }
 
     def position(line: Int): Position.T =
       source_position(line) getOrElse
         Position.Line_File(line, source_file.getOrElse(tex_file.implode))
   }
 
 
   /* latex log */
 
   def latex_errors(dir: Path, root_name: String): List[String] = {
-    val root_log_path = dir + Path.explode(root_name).ext("log")
+    val root_log_path = dir + Path.explode(root_name).log
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
         yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
     }
     else Nil
   }
 
   def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = {
     val seen_files = Synchronized(Map.empty[JFile, Tex_File])
 
     def check_tex_file(path: Path): Option[Tex_File] =
       seen_files.change_result(seen =>
         seen.get(path.file) match {
           case None =>
             if (path.is_file) {
               val tex_file = read_tex_file(path)
               (Some(tex_file), seen + (path.file -> tex_file))
             }
             else (None, seen)
           case some => (some, seen)
         })
 
     def tex_file_position(path: Path, line: Int): Position.T =
       check_tex_file(path) match {
         case Some(tex_file) => tex_file.position(line)
         case None => Position.Line_File(line, path.implode)
       }
 
     object File_Line_Error {
       val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
       def unapply(line: String): Option[(Path, Int, String)] =
         line match {
           case Pattern(file, Value.Int(line), message) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val file = (dir + Path.explode(path)).canonical
               val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
               if (file.is_file) Some((file, line, msg)) else None
             }
             else None
           case _ => None
         }
     }
 
     val Line_Error = """^l\.\d+ (.*)$""".r
     val More_Error =
       List(
         "<argument>",
         "<template>",
         "<recently read>",
         "<to be read again>",
         "<inserted text>",
         "<output>",
         "<everypar>",
         "<everymath>",
         "<everydisplay>",
         "<everyhbox>",
         "<everyvbox>",
         "<everyjob>",
         "<everycr>",
         "<mark>",
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
     val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r
     val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
 
     val error_ignore =
       Set(
         "See the LaTeX manual or LaTeX Companion for explanation.",
         "Type  H <return>  for immediate help.")
 
     def error_suffix1(lines: List[String]): Option[String] = {
       val lines1 =
         lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
         case (Line_Error(msg), i) =>
           cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
     }
     def error_suffix2(lines: List[String]): Option[String] =
       lines match {
         case More_Error(msg) :: _ => Some(msg)
         case _ => None
       }
 
     @tailrec def filter(
       lines: List[String],
       result: List[(String, Position.T)]
     ) : List[(String, Position.T)] = {
       lines match {
         case File_Line_Error((file, line, msg1)) :: rest1 =>
           val pos = tex_file_position(file, line)
           val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
           filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
         case Bad_Font(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case Bad_File(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }
     }
 
     filter(Line.logical_lines(root_log), Nil)
   }
 }
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,1649 +1,1649 @@
 /*  Title:      Pure/Thy/sessions.scala
     Author:     Makarius
 
 Cumulative session information.
 */
 
 package isabelle
 
 import java.io.{File => JFile}
 import java.sql.SQLException
 
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.collection.mutable
 
 
 object Sessions {
   /* session and theory names */
 
   val ROOTS: Path = Path.explode("ROOTS")
   val ROOT: Path = Path.explode("ROOT")
 
   val roots_name: String = "ROOTS"
   val root_name: String = "ROOT"
   val theory_import: String = "Pure.Sessions"
 
   val UNSORTED = "Unsorted"
   val DRAFT = "Draft"
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
   def illegal_session(name: String): Boolean = name == "" || name == DRAFT
   def illegal_theory(name: String): Boolean =
     name == root_name || File_Format.registry.theory_excluded(name)
 
 
   /* ROOTS file format */
 
   class ROOTS_File_Format extends File_Format {
     val format_name: String = roots_name
     val file_ext = ""
 
     override def detect(name: String): Boolean =
       Url.get_base_name(name) match {
         case Some(base_name) => base_name == roots_name
         case None => false
       }
 
     override def theory_suffix: String = "ROOTS_file"
     override def theory_content(name: String): String =
       """theory "ROOTS" imports Pure begin ROOTS_file "." end"""
     override def theory_excluded(name: String): Boolean = name == "ROOTS"
   }
 
 
   /* source files */
 
   sealed case class Source_File(
     name: String,
     digest: SHA1.Digest,
     compressed: Boolean,
     body: Bytes,
     cache: Compress.Cache
   ) {
     override def toString: String = name
 
     def bytes: Bytes = if (compressed) body.uncompress(cache = cache) else body
   }
 
   object Sources {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
     val digest = SQL.Column.string("digest")
     val compressed = SQL.Column.bool("compressed")
     val body = SQL.Column.bytes("body")
 
     val table =
       SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
       "WHERE " + Sources.session_name.equal(session_name) +
         (if (name == "") "" else " AND " + Sources.name.equal(name))
 
     def load(session_base: Base, cache: Compress.Cache = Compress.Cache.none): Sources =
       new Sources(
         session_base.session_sources.foldLeft(Map.empty) {
           case (sources, (path, digest)) =>
             def err(): Nothing = error("Incoherent digest for source file: " + path)
             val name = File.symbolic_path(path)
             sources.get(name) match {
               case Some(source_file) =>
                 if (source_file.digest == digest) sources else err()
               case None =>
                 val bytes = Bytes.read(path)
                 if (bytes.sha1_digest == digest) {
                   val (compressed, body) =
                     bytes.maybe_compress(Compress.Options_Zstd(), cache = cache)
                   val file = Source_File(name, digest, compressed, body, cache)
                   sources + (name -> file)
                 }
                 else err()
             }
         })
   }
 
   class Sources private(rep: Map[String, Source_File]) extends Iterable[Source_File] {
     override def toString: String = rep.values.toList.sortBy(_.name).mkString("Sources(", ", ", ")")
     override def iterator: Iterator[Source_File] = rep.valuesIterator
 
     def get(name: String): Option[Source_File] = rep.get(name)
     def apply(name: String): Source_File =
       get(name).getOrElse(error("Missing session sources entry " + quote(name)))
   }
 
 
   /* base info */
 
   object Base {
     val bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
   }
 
   sealed case class Base(
     session_name: String = "",
     session_pos: Position.T = Position.none,
     proper_session_theories: List[Document.Node.Name] = Nil,
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,  // cumulative imports
     used_theories: List[(Document.Node.Name, Options)] = Nil,  // new imports
     theory_load_commands: Map[String, List[Command_Span.Span]] = Map.empty,
     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,
     session_sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil
   ) {
     def session_entry: (String, Base) = session_name -> this
 
     override def toString: String = "Sessions.Base(" + print_body + ")"
     def print_body: String =
       "session_name = " + quote(session_name) +
       ", loaded_theories = " + loaded_theories.size +
       ", used_theories = " + used_theories.length
 
     def all_document_theories: List[Document.Node.Name] =
       proper_session_theories ::: document_theories
 
     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 theory_syntax(name: Document.Node.Name): Outer_Syntax =
       loaded_theory_syntax(name) getOrElse overall_syntax
 
     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
 
   /* background context */
 
   sealed case class Background(
     base: Base,
     sessions_structure: Structure = Structure.empty,
     errors: List[String] = Nil,
     infos: List[Info] = Nil
   ) {
     def session_name: String = base.session_name
     def info: Info = sessions_structure(session_name)
 
     def check_errors: Background =
       if (errors.isEmpty) this
       else error(cat_lines(errors))
   }
 
   def background0(session: String): Background =
     Background(Base(session_name = session))
 
   def background(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
   ): Background = {
     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) && selected_sessions.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(
               Info.make(
                 Chapter_Defs.empty,
                 info.options,
                 augment_options = _ => Nil,
                 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,
                   export_classpath = 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)
 
     Background(deps1(session1), sessions_structure = full_sessions1,
       errors = deps1.errors, infos = infos1)
   }
 
 
   /* source dependencies */
 
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
     def background(session: String): Background =
       Background(base = apply(session), sessions_structure = sessions_structure, errors = errors)
 
     def is_empty: Boolean = session_bases.keysIterator.forall(_.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 session_sources(name: String): List[SHA1.Digest] =
       session_bases(name).session_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.session_pos)
       ).toList
 
     def check_errors: Deps =
       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
 
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
   }
 
   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 session_bases =
       sessions_structure.imports_topological_order.foldLeft(Map(Base.bootstrap.session_entry)) {
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
           val info = sessions_structure(session_name)
           try {
             val deps_base = info.deps_base(session_bases)
             val session_background =
               Background(base = deps_base, sessions_structure = sessions_structure)
             val resources = new Resources(session_background)
 
             if (verbose || list_files) {
               val groups =
                 if (info.groups.isEmpty) ""
                 else info.groups.mkString(" (", " ", ")")
               progress.echo("Session " + info.chapter + "/" + session_name + groups)
             }
 
             val dependencies = resources.session_dependencies(info)
 
             val overall_syntax = dependencies.overall_syntax
 
             val proper_session_theories =
               dependencies.theories.filter(name =>
                 sessions_structure.theory_qualifier(name) == session_name)
 
             val theory_files = dependencies.theories.map(_.path)
 
             val (load_commands, load_commands_errors) =
               try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) }
               catch { case ERROR(msg) => (Nil, List(msg)) }
 
             val theory_load_commands =
               (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap
 
             val loaded_files: List[(String, List[Path])] =
               for ((name, spans) <- load_commands) yield {
                 val (theory, files) = dependencies.loaded_files(name, spans)
                 theory -> files.map(file => Path.explode(file.node))
               }
 
             val document_files =
               for ((path1, path2) <- info.document_files)
                 yield info.dir + path1 + path2
 
             val session_files =
               (theory_files ::: loaded_files.flatMap(_._2) ::: document_files).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 = sessions_structure.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 => sessions_structure.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 =
                 required_subgraph.topological_order.foldLeft(Graph_Display.empty_graph) {
                   case (g, session) =>
                     val a = session_node(session)
                     val bs = required_subgraph.imm_preds(session).toList.map(session_node)
                     bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
                 }
 
               dependencies.entries.foldLeft(graph0) {
                 case (g, entry) =>
                   val a = node(entry.name)
                   val bs = entry.header.imports.map(node).filterNot(_ == a)
                   bs.foldLeft((a :: bs).foldLeft(g)(_.default_node(_, Nil)))(_.add_edge(_, a))
               }
             }
 
             val known_theories =
               dependencies.entries.iterator.map(entry => entry.name.theory -> entry).
                 foldLeft(deps_base.known_theories)(_ + _)
 
             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 = sessions_structure.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 build_hierarchy =
                     if (sessions_structure.build_graph.defined(session_name)) {
                       sessions_structure.build_hierarchy(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 = sessions_structure.theory_qualifier(name)
                       if (proper_session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
                       else if (
                         !build_hierarchy.contains(qualifier) &&
                         !dependencies.theories.contains(name)
                       ) {
                         err("Document theory from other session not imported properly:")
                       }
                       else None
                   }
               })
             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 <- proper_session_theories.iterator
                   path = Path.explode(name.master_dir)
                   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 <- proper_session_theories.iterator
                   name1 <- resources.find_theory_node(name.theory)
                   if name.node != name1.node
                 } yield {
                   "Incoherent theory file import:\n  " + quote(name.node) +
                     " vs. \n  " + quote(name1.node)
                 }).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 = info.bibtex_entries.errors
 
             val base =
               Base(
                 session_name = info.name,
                 session_pos = info.pos,
                 proper_session_theories = proper_session_theories,
                 document_theories = document_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.theories_adjunct,
                 theory_load_commands = theory_load_commands,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 session_sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
                 errors = dependencies.errors ::: load_commands_errors ::: import_errors :::
                   document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
                   bibtex_errors)
 
             session_bases + base.session_entry
           }
           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)
   }
 
 
   /* cumulative session info */
 
   sealed case class Chapter_Info(
     name: String,
     pos: Position.T,
     groups: List[String],
     description: String,
     sessions: List[String]
   )
 
   object Info {
     def make(
       chapter_defs: Chapter_Defs,
       options: Options,
       augment_options: String => List[Options.Spec],
       dir_selected: Boolean,
       dir: Path,
       chapter: String,
       entry: Session_Entry
     ): Info = {
       try {
         val name = entry.name
 
         if (illegal_session(name)) error("Illegal session name " + quote(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 entry_options = entry.options ::: augment_options(name)
         val session_options = options ++ entry_options
 
         val theories =
           entry.theories.map({ case (opts, thys) =>
             (session_options ++ opts,
               thys.map({ case ((thy, pos), _) =>
                 val thy_name = Thy_Header.import_name(thy)
                 if (illegal_theory(thy_name)) {
                   error("Illegal theory name " + quote(thy_name) + 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_no_position,
               entry.document_files)
             .toString)
 
         val chapter_groups = chapter_defs(chapter).groups
         val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains)
 
         Info(name, chapter, dir_selected, entry.pos, groups, session_path,
           entry.parent, entry.description, directories, session_options,
           entry.imports, theories, global_theories, entry.document_theories, document_files,
           export_files, entry.export_classpath, meta_digest)
       }
       catch {
         case ERROR(msg) =>
           error(msg + "\nThe error(s) above occurred in session entry " +
             quote(entry.name) + Position.here(entry.pos))
       }
     }
   }
 
   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])],
     export_classpath: 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 =
           (for {
             base <- imports_bases.iterator
             (_, entry) <- base.known_theories.iterator
           } yield (entry.name.theory -> entry)).foldLeft(parent_base.known_theories)(_ + _),
         known_loaded_files =
           imports_bases.iterator.map(_.known_loaded_files).
             foldLeft(parent_base.known_loaded_files)(_ ++ _))
     }
 
     def dirs: List[Path] = dir :: directories
 
     def main_group: Boolean = groups.contains("main")
     def doc_group: Boolean = groups.contains("doc")
 
     def timeout_ignored: Boolean =
       !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
 
     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" => true
         case doc => error("Bad document specification " + quote(doc))
       }
 
     def document_variants: List[Document_Build.Document_Variant] = {
       val variants =
         Library.space_explode(':', options.string("document_variants")).
           map(Document_Build.Document_Variant.parse)
 
       val dups = Library.duplicates(variants.map(_.name))
       if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
 
       variants
     }
 
     def document_echo: Boolean = options.bool("document_echo")
 
     def documents: List[Document_Build.Document_Variant] = {
       val variants = document_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: Bibtex.Entries =
       (for {
         (document_dir, file) <- document_files.iterator
         if File.is_bib(file.file_name)
       } yield {
         val path = dir + document_dir + file
         Bibtex.Entries.parse(File.read(path), start = Token.Pos.file(File.standard_path(path)))
       }).foldRight(Bibtex.Entries.empty)(_ ::: _)
 
     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)
   }
 
   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))
   }
 
   object Structure {
     val empty: Structure = make(Options.empty)
 
     def make(
       options: Options,
       augment_options: String => List[Options.Spec] = _ => Nil,
       roots: List[Root_File] = Nil,
       infos: List[Info] = Nil
     ): Structure = {
       val chapter_defs: Chapter_Defs =
         roots.foldLeft(Chapter_Defs.empty) {
           case (defs1, root) =>
             root.entries.foldLeft(defs1) {
               case (defs2, entry: Chapter_Def) => defs2 + entry
               case (defs2, _) => defs2
             }
         }
 
       val root_infos = {
         var chapter = UNSORTED
         val root_infos = new mutable.ListBuffer[Info]
         for (root <- roots) {
           root.entries.foreach {
             case entry: Chapter_Entry => chapter = entry.name
             case entry: Session_Entry =>
               root_infos +=
                 Info.make(chapter_defs, options, augment_options,
                   root.select, root.dir, chapter, entry)
             case _ =>
           }
           chapter = UNSORTED
         }
         root_infos.toList
       }
 
       val info_graph =
         (root_infos ::: infos).foldLeft(Graph.string[Info]) {
           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)
         }
 
       def augment_graph(
         graph: Graph[String, Info],
         kind: String,
         edges: Info => Iterable[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.iterator.foldLeft(graph) {
           case (g, (name, (info, _))) =>
             edges(info).foldLeft(g)(add_edge(info.pos, name, _, _))
         }
       }
 
       val build_graph = augment_graph(info_graph, "parent", _.parent)
       val imports_graph = augment_graph(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] =
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           dir <- info.dirs.iterator
         } yield (info, dir)).foldLeft(Map.empty[JFile, String]) {
             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] =
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
           thy <- info.global_theories.iterator }
           yield (info, thy)
         ).foldLeft(Thy_Header.bootstrap_global_theories.toMap) {
             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(chapter_defs, session_positions, session_directories,
         global_theories, build_graph, imports_graph)
     }
   }
 
   final class Structure private[Sessions](
     chapter_defs: Chapter_Defs,
     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 known_chapters: List[Chapter_Info] = {
       val chapter_sessions =
         Multi_Map.from(
           for ((_, (info, _)) <- build_graph.iterator)
             yield info.chapter -> info.name)
       val chapters1 =
         (for (entry <- chapter_defs.list.iterator) yield {
           val sessions = chapter_sessions.get_list(entry.name)
           Chapter_Info(entry.name, entry.pos, entry.groups, entry.description, sessions.sorted)
         }).toList
       val chapters2 =
         (for {
           (name, sessions) <- chapter_sessions.iterator_list
           if !chapters1.exists(_.name == name)
         } yield Chapter_Info(name, Position.none, Nil, "", sessions.sorted)).toList.sortBy(_.name)
       chapters1 ::: chapters2
     }
 
     def relevant_chapters: List[Chapter_Info] = known_chapters.filter(_.sessions.nonEmpty)
 
     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 theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory)
 
     def check_sessions(names: List[String]): Unit = {
       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) || info.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 info.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(chapter_defs, 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_hierarchy(session: String): List[String] =
       if (build_graph.defined(session)) build_graph.all_preds(List(session))
       else List(session)
 
     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
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
   }
 
 
   /* parser */
 
   private val CHAPTER_DEFINITION = "chapter_definition"
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   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"
   private val EXPORT_CLASSPATH = "export_classpath"
 
   val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + "in" +
       GLOBAL +
       (CHAPTER_DEFINITION, Keyword.THY_DECL) +
       (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) +
       (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
 
   abstract class Entry
   object Chapter_Def {
     def empty(chapter: String): Chapter_Def = Chapter_Def(Position.none, chapter, Nil, "")
   }
   sealed case class Chapter_Def(
     pos: Position.T,
     name: String,
     groups: List[String],
     description: String
   ) extends Entry
   sealed case class Chapter_Entry(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])],
     export_classpath: 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) })) })
     def document_theories_no_position: List[String] =
       document_theories.map(_._1)
   }
 
   object Chapter_Defs {
     val empty: Chapter_Defs = new Chapter_Defs(Nil)
   }
 
   class Chapter_Defs private(rev_list: List[Chapter_Def]) {
     def list: List[Chapter_Def] = rev_list.reverse
 
     override def toString: String =
       list.map(_.name).mkString("Chapter_Defs(", ", ", ")")
 
     def get(chapter: String): Option[Chapter_Def] =
       rev_list.find(_.name == chapter)
 
     def apply(chapter: String): Chapter_Def =
       get(chapter) getOrElse Chapter_Def.empty(chapter)
 
     def + (entry: Chapter_Def): Chapter_Defs =
       get(entry.name) match {
         case None => new Chapter_Defs(entry :: rev_list)
         case Some(old_entry) =>
           error("Duplicate chapter definition " + quote(entry.name) +
             Position.here(old_entry.pos) + Position.here(entry.pos))
       }
   }
 
   private object Parsers extends Options.Parsers {
     private val groups: Parser[List[String]] =
       ($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)
 
     private val description: Parser[String] =
       ($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")
 
     private val chapter_def: Parser[Chapter_Def] =
       command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ groups ~ description) ^^
         { case _ ~ ((a, pos) ~ b ~ c) => Chapter_Def(pos, a, b, c) }
 
     private val chapter_entry: Parser[Chapter_Entry] =
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(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 document_theories =
         $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x }
 
       val document_files =
         $$$(DOCUMENT_FILES) ~! (in_path_parens("document") ~ rep1(path)) ^^
           { case _ ~ (x ~ y) => y.map((x, _)) }
 
       val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
 
       val export_files =
         $$$(EXPORT_FILES) ~! (in_path_parens("export") ~ prune ~ rep1(embedded)) ^^
           { case _ ~ (x ~ y ~ z) => (x, y, z) }
 
       val export_classpath =
         $$$(EXPORT_CLASSPATH) ~! (rep1(embedded) | success(List("*:classpath/*.jar"))) ^^
           { case _ ~ x => x }
 
       command(SESSION) ~!
         (position(session_name) ~ groups ~ in_path(".") ~
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ description ~
               (($$$(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) ~
               opt(export_classpath)))) ^^
         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l ~ m))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l, m.getOrElse(Nil)) }
     }
 
     def parse_root(path: Path): List[Entry] = {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
       val parser: Parser[Entry] = chapter_def | chapter_entry | session_entry
       parse_all(rep(parser), Token.reader(toks, start)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
     }
   }
 
   def parse_root(path: Path): List[Entry] = Parsers.parse_root(path)
 
   def parse_root_entries(path: Path): List[Session_Entry] =
     Parsers.parse_root(path).flatMap(Library.as_subclass(classOf[Session_Entry]))
 
   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 */
 
   def is_session_dir(dir: Path): Boolean =
     (dir + ROOT).is_file || (dir + ROOTS).is_file
 
   def check_session_dir(dir: Path): Path =
     if (is_session_dir(dir)) File.pwd() + dir.expand
     else {
       error("Bad session root directory: " + dir.expand.toString +
         "\n  (missing \"ROOT\" or \"ROOTS\")")
     }
 
   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {
     val default_dirs = Components.directories().filter(is_session_dir)
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }
 
   sealed case class Root_File(path: Path, select: Boolean) {
     val key: JFile = path.canonical_file
     def dir: Path = path.dir
 
     lazy val entries: List[Entry] = Parsers.parse_root(path)
   }
 
   def load_root_files(
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil
   ): List[Root_File] = {
     def load_dir(select: Boolean, dir: Path): List[Root_File] =
       load_root(select, dir) ::: load_roots(select, dir)
 
     def load_root(select: Boolean, dir: Path): List[Root_File] = {
       val root = dir + ROOT
       if (root.is_file) List(Root_File(root, select)) else Nil
     }
 
     def load_roots(select: Boolean, dir: Path): List[Root_File] = {
       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 raw_roots: List[Root_File] =
       for {
         (select, dir) <- directories(dirs, select_dirs)
         root <- load_dir(select, check_session_dir(dir))
       } yield root
 
     var next_root = 0
     var seen_roots = Map.empty[JFile, (Root_File, Int)]
     for (root <- raw_roots) {
       seen_roots.get(root.key) match {
         case None =>
           seen_roots += (root.key -> (root, next_root))
           next_root += 1
         case Some((root0, next0)) =>
           val root1 = root0.copy(select = root0.select || root.select)
           seen_roots += (root0.key -> (root1, next0))
       }
     }
     seen_roots.valuesIterator.toList.sortBy(_._2).map(_._1)
   }
 
   def load_structure(
     options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Info] = Nil,
     augment_options: String => List[Options.Spec] = _ => Nil
   ): Structure = {
     val roots = load_root_files(dirs = dirs, select_dirs = select_dirs)
     Structure.make(options, augment_options, roots = roots, infos = infos)
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions",
     Scala_Project.here,
     { 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 build_graph = 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
     -b           follow session build dependencies (default: source imports)
     -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),
         "b" -> (_ => build_graph = 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)
 
       val order =
         if (build_graph) sessions_structure.build_topological_order
         else sessions_structure.imports_topological_order
       for (name <- order) Output.writeln(name, stdout = true)
     })
 
 
 
   /** 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 uuid = SQL.Column.string("uuid")
     val build_columns = List(sources, input_heaps, output_heap, return_code, uuid)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
 
     val augment_table: PostgreSQL.Source =
       "ALTER TABLE IF EXISTS " + table.ident +
       " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
   }
 
   def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
     new Store(options, cache)
 
   class Store private[Sessions](val options: Options, val cache: Term.Cache) {
     store =>
 
     override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
 
     /* 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 database(name: String): Path = Path.basic("log") + Path.basic(name).db
     def log(name: String): Path = Path.basic("log") + Path.basic(name)
-    def log_gz(name: String): Path = log(name).ext("gz")
+    def log_gz(name: String): Path = log(name).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(): Unit = 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(ML_Heap.read_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 => "  " + File.standard_path(dir))))
 
 
     /* database */
 
     def find_database(name: String): Option[Path] =
       input_dirs.map(_ + database(name)).find(_.is_file)
 
     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,
       server: Boolean = database_server
     ): Option[SQL.Database] = {
       def check(db: SQL.Database): Option[SQL.Database] =
         if (output || session_info_exists(db)) Some(db) else { db.close(); None }
 
       if (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 error_database(name: String): Nothing =
       error("Missing build database for session " + quote(name))
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
       try_open_database(name, output = output) getOrElse error_database(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 = cache)
 
 
     /* session info */
 
     def init_session_info(db: SQL.Database, name: String): Unit = {
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
         if (db.isInstanceOf[PostgreSQL.Database]) {
           db.using_statement(Session_Info.augment_table)(_.execute())
         }
 
         db.create_table(Sources.table)
         db.using_statement(Sources.table.delete(Sources.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())
 
         db.create_table(Document_Build.Data.table)
         db.using_statement(
           Document_Build.Data.table.delete(
             Document_Build.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 =
       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,
       session_name: String,
       sources: Sources,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info
     ): Unit = {
       db.transaction {
         write_sources(db, session_name, sources)
         db.using_statement(Session_Info.table.insert()) { stmt =>
           stmt.string(1) = session_name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
           stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
           stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
           stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
           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.string(12) = build.uuid
           stmt.execute()
         }
       }
     }
 
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
       Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = 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_theories(db: SQL.Database, name: String): List[String] =
       read_theory_timings(db, name).flatMap(Markup.Name.unapply)
 
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = 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(Nil,
           Session_Info.session_name.where_equal(name))) { stmt =>
           val res = stmt.execute_query()
           if (!res.next()) None
           else {
             val uuid =
               try { Option(res.string(Session_Info.uuid)).getOrElse("") }
               catch { case _: SQLException => "" }
             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),
                 uuid))
           }
         }
       }
       else None
     }
 
 
     /* session sources */
 
     def write_sources(db: SQL.Database, session_name: String, sources: Sources): Unit = {
       for (source_file <- sources) {
         db.using_statement(Sources.table.insert()) { stmt =>
           stmt.string(1) = session_name
           stmt.string(2) = source_file.name
           stmt.string(3) = source_file.digest.toString
           stmt.bool(4) = source_file.compressed
           stmt.bytes(5) = source_file.body
           stmt.execute()
         }
       }
     }
 
     def read_sources(
       db: SQL.Database,
       session_name: String,
       name: String = ""
     ): List[Source_File] = {
       val select =
         Sources.table.select(Nil,
           Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name)))
       db.using_statement(select) { stmt =>
         (stmt.execute_query().iterator { res =>
           val res_name = res.string(Sources.name)
           val digest = SHA1.fake_digest(res.string(Sources.digest))
           val compressed = res.bool(Sources.compressed)
           val body = res.bytes(Sources.body)
           Source_File(res_name, digest, compressed, body, cache.compress)
         }).toList
       }
     }
   }
 }