# HG changeset patch
# User wenzelm
# Date 1705763375 -3600
# Node ID c67b47cd41dcf599029a6396e17ca1cb7efe08fa
# Parent  c7a98469c0e7176c5333a2e3df4fc3360082017d
clarified directories;

diff -r c7a98469c0e7 -r c67b47cd41dc etc/build.props
--- a/etc/build.props	Sat Jan 20 15:07:41 2024 +0100
+++ b/etc/build.props	Sat Jan 20 16:09:35 2024 +0100
@@ -77,6 +77,7 @@
   src/Pure/GUI/wrap_panel.scala \
   src/Pure/General/antiquote.scala \
   src/Pure/General/base64.scala \
+  src/Pure/General/bibtex.scala \
   src/Pure/General/bytes.scala \
   src/Pure/General/cache.scala \
   src/Pure/General/codepoint.scala \
@@ -96,6 +97,7 @@
   src/Pure/General/js.scala \
   src/Pure/General/json.scala \
   src/Pure/General/json_api.scala \
+  src/Pure/General/latex.scala \
   src/Pure/General/linear_set.scala \
   src/Pure/General/logger.scala \
   src/Pure/General/long_name.scala \
@@ -191,9 +193,7 @@
   src/Pure/System/scala.scala \
   src/Pure/System/system_channel.scala \
   src/Pure/System/tty_loop.scala \
-  src/Pure/Thy/bibtex.scala \
   src/Pure/Thy/document_build.scala \
-  src/Pure/Thy/latex.scala \
   src/Pure/Thy/thy_element.scala \
   src/Pure/Thy/thy_header.scala \
   src/Pure/Thy/thy_syntax.scala \
diff -r c7a98469c0e7 -r c67b47cd41dc src/Pure/General/bibtex.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/bibtex.ML	Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,134 @@
+(*  Title:      Pure/General/bibtex.ML
+    Author:     Makarius
+
+Support for BibTeX.
+*)
+
+signature BIBTEX =
+sig
+  val check_database:
+    Position.T -> string -> (string * Position.T) list * (string * Position.T) list
+  val check_database_output: Position.T -> string -> unit
+  val check_bibtex_entry: Proof.context -> string * Position.T -> unit
+  val cite_macro: string Config.T
+  val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
+end;
+
+structure Bibtex: BIBTEX =
+struct
+
+(* check database *)
+
+type message = string * Position.T;
+
+fun check_database pos0 database =
+  \<^scala>\<open>bibtex_check_database\<close> database
+  |> YXML.parse_body
+  |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
+  |> (apply2 o map o apsnd)
+      (fn pos => Position.of_properties (pos @ Position.properties_of pos0));
+
+fun check_database_output pos0 database =
+  let val (errors, warnings) = check_database pos0 database in
+    errors |> List.app (fn (msg, pos) =>
+      Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
+    warnings |> List.app (fn (msg, pos) =>
+      warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
+  end;
+
+
+(* check bibtex entry *)
+
+fun check_bibtex_entry ctxt (name, pos) =
+  let
+    fun warn () =
+      if Context_Position.is_visible ctxt then
+        warning ("Unknown session context: cannot check Bibtex entry " ^
+          quote name ^ Position.here pos)
+      else ();
+    fun decode yxml =
+      let
+        val props = XML.Decode.properties (YXML.parse_body yxml);
+        val name = Properties.get_string props Markup.nameN;
+        val pos = Position.of_properties props;
+      in (name, pos) end;
+  in
+    if name = "*" then ()
+    else
+      (case Position.id_of pos of
+        NONE => warn ()
+      | SOME id =>
+          (case \<^scala>\<open>bibtex_session_entries\<close> [id] of
+            [] => warn ()
+          | _ :: entries =>
+              Completion.check_entity Markup.bibtex_entryN (map decode entries)
+                ctxt (name, pos) |> ignore))
+  end;
+
+
+(* document antiquotations *)
+
+val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "");
+fun get_cite_macro ctxt = Config.get ctxt cite_macro;
+
+val _ =
+  Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro));
+
+
+local
+
+val parse_citations = Parse.and_list1 (Parse.position Parse.name);
+
+fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
+  let
+    val loc = the_default Input.empty opt_loc;
+    val _ = Context_Position.reports ctxt (Document_Output.document_reports loc);
+    val _ = List.app (check_bibtex_entry ctxt) citations;
+
+    val kind = if macro_name = "" then get_kind ctxt else macro_name;
+    val location = Document_Output.output_document ctxt {markdown = false} loc;
+  in Latex.cite {kind = kind, citations = citations, location = location} end;
+
+fun cite_command_old ctxt get_kind args =
+  let
+    val _ =
+      if Context_Position.is_visible ctxt then
+        legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^
+          Position.here_list (map snd (snd args)))
+      else ();
+  in cite_command ctxt get_kind (args, "") end;
+
+val cite_keywords =
+  Thy_Header.bootstrap_keywords
+  |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]);
+
+fun cite_command_embedded ctxt get_kind input =
+  let
+    val parser =
+      Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations --
+        Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) "";
+    val args = Parse.read_embedded ctxt cite_keywords parser input;
+  in cite_command ctxt get_kind args end;
+
+fun cite_command_parser get_kind =
+  Scan.option Args.cartouche_input -- parse_citations
+    >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) ||
+  Parse.embedded_input
+    >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);
+
+in
+
+fun cite_antiquotation binding get_kind =
+  Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind))
+    (fn ctxt => fn cmd => cmd ctxt);
+
+end;
+
+val _ =
+  Theory.setup
+   (cite_antiquotation \<^binding>\<open>cite\<close> get_cite_macro #>
+    cite_antiquotation \<^binding>\<open>nocite\<close> (K "nocite") #>
+    cite_antiquotation \<^binding>\<open>citet\<close> (K "citet") #>
+    cite_antiquotation \<^binding>\<open>citep\<close> (K "citep"));
+
+end;
diff -r c7a98469c0e7 -r c67b47cd41dc src/Pure/General/bibtex.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/bibtex.scala	Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,855 @@
+/*  Title:      Pure/General/bibtex.scala
+    Author:     Makarius
+
+Support for BibTeX.
+*/
+
+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).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.capitalized(msg) + " in entry " + quote(name), chunk_pos(name))))
+              case (Warning(msg), Warning_Line(Value.Int(l))) =>
+                Some((false, (Word.capitalized(msg), get_line_pos(l))))
+              case (Warning(msg), _) =>
+                Some((false, (Word.capitalized(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(other.entries ::: entries, other.errors ::: 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.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_proper(title, " -h " + Bash.string(title) + " ") +
+          " " + 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] =
+    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_proper(location, 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 = 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 -r c7a98469c0e7 -r c67b47cd41dc src/Pure/General/latex.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/latex.ML	Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,262 @@
+(*  Title:      Pure/General/latex.ML
+    Author:     Makarius
+
+Support for LaTeX.
+*)
+
+signature LATEX =
+sig
+  type text = XML.body
+  val text: string * Position.T -> text
+  val string: string -> text
+  val block: text -> XML.tree
+  val output: text -> text
+  val macro0: string -> text
+  val macro: string -> text -> text
+  val environment: string -> text -> text
+  val output_name: string -> string
+  val output_ascii: string -> string
+  val output_ascii_breakable: string -> string -> string
+  val output_symbols: Symbol.symbol list -> string
+  val output_syms: string -> string
+  val symbols: Symbol_Pos.T list -> text
+  val symbols_output: Symbol_Pos.T list -> text
+  val isabelle_body: string -> text -> text
+  val theory_entry: string -> string
+  val cite: {kind: string, citations: (string * Position.T) list, location: text} -> text
+  type index_item = {text: text, like: string}
+  type index_entry = {items: index_item list, def: bool}
+  val index_entry: index_entry -> text
+  val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
+  val latexN: string
+  val latex_markup: string * Properties.T -> Markup.output
+end;
+
+structure Latex: LATEX =
+struct
+
+(* text with positions *)
+
+type text = XML.body;
+
+fun text (s, pos) =
+  if s = "" then []
+  else if pos = Position.none then [XML.Text s]
+  else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
+
+fun string s = text (s, Position.none);
+
+fun block body = XML.Elem (Markup.document_latex, body);
+
+fun output body = [XML.Elem (Markup.latex_output, body)];
+
+fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
+fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
+fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
+
+
+(* output name for LaTeX macros *)
+
+val output_name =
+  translate_string
+    (fn "_" => "UNDERSCORE"
+      | "'" => "PRIME"
+      | "0" => "ZERO"
+      | "1" => "ONE"
+      | "2" => "TWO"
+      | "3" => "THREE"
+      | "4" => "FOUR"
+      | "5" => "FIVE"
+      | "6" => "SIX"
+      | "7" => "SEVEN"
+      | "8" => "EIGHT"
+      | "9" => "NINE"
+      | s => s);
+
+fun enclose_name bg en = enclose bg en o output_name;
+
+
+(* output verbatim ASCII *)
+
+val output_ascii =
+  translate_string
+    (fn " " => "\\ "
+      | "\t" => "\\ "
+      | "\n" => "\\isanewline\n"
+      | s =>
+          s
+          |> member_string "\"#$%&',-<>\\^_`{}~" s ? enclose "{\\char`\\" "}"
+          |> suffix "{\\kern0pt}");
+
+fun output_ascii_breakable sep =
+  space_explode sep
+  #> map output_ascii
+  #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
+
+
+(* output symbols *)
+
+local
+
+val char_table =
+  Symtab.make
+   [("\007", "{\\isacharbell}"),
+    ("!", "{\\isacharbang}"),
+    ("\"", "{\\isachardoublequote}"),
+    ("#", "{\\isacharhash}"),
+    ("$", "{\\isachardollar}"),
+    ("%", "{\\isacharpercent}"),
+    ("&", "{\\isacharampersand}"),
+    ("'", "{\\isacharprime}"),
+    ("(", "{\\isacharparenleft}"),
+    (")", "{\\isacharparenright}"),
+    ("*", "{\\isacharasterisk}"),
+    ("+", "{\\isacharplus}"),
+    (",", "{\\isacharcomma}"),
+    ("-", "{\\isacharminus}"),
+    (".", "{\\isachardot}"),
+    ("/", "{\\isacharslash}"),
+    (":", "{\\isacharcolon}"),
+    (";", "{\\isacharsemicolon}"),
+    ("<", "{\\isacharless}"),
+    ("=", "{\\isacharequal}"),
+    (">", "{\\isachargreater}"),
+    ("?", "{\\isacharquery}"),
+    ("@", "{\\isacharat}"),
+    ("[", "{\\isacharbrackleft}"),
+    ("\\", "{\\isacharbackslash}"),
+    ("]", "{\\isacharbrackright}"),
+    ("^", "{\\isacharcircum}"),
+    ("_", "{\\isacharunderscore}"),
+    ("`", "{\\isacharbackquote}"),
+    ("{", "{\\isacharbraceleft}"),
+    ("|", "{\\isacharbar}"),
+    ("}", "{\\isacharbraceright}"),
+    ("~", "{\\isachartilde}")];
+
+fun output_chr " " = "\\ "
+  | output_chr "\t" = "\\ "
+  | output_chr "\n" = "\\isanewline\n"
+  | output_chr c =
+      (case Symtab.lookup char_table c of
+        SOME s => s ^ "{\\kern0pt}"
+      | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
+
+fun output_sym sym =
+  (case Symbol.decode sym of
+    Symbol.Char s => output_chr s
+  | Symbol.UTF8 s => s
+  | Symbol.Sym s => enclose_name "{\\isasym" "}" s
+  | Symbol.Control s => enclose_name "\\isactrl" " " s
+  | Symbol.Malformed s => error (Symbol.malformed_msg s)
+  | Symbol.EOF => error "Bad EOF symbol");
+
+open Basic_Symbol_Pos;
+
+val scan_latex_length =
+  Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
+    >> (Symbol.length o map Symbol_Pos.symbol) ||
+  $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
+
+val scan_latex =
+  $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
+    >> (implode o map Symbol_Pos.symbol) ||
+  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
+
+fun read scan syms =
+  Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
+
+in
+
+val length_symbols =
+  Integer.build o fold Integer.add o these o read scan_latex_length;
+
+fun output_symbols syms =
+  if member (op =) syms Symbol.latex then
+    (case read scan_latex syms of
+      SOME ss => implode ss
+    | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
+  else implode (map output_sym syms);
+
+val output_syms = output_symbols o Symbol.explode;
+
+end;
+
+fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
+fun symbols_output syms =
+  text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
+
+
+(* theory presentation *)
+
+fun isabelle_body name =
+  XML.enclose
+   ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
+   "%\n\\end{isabellebody}%\n";
+
+fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
+
+
+(* cite: references to bibliography *)
+
+fun cite {kind, location, citations} =
+  let
+    val _ =
+      citations |> List.app (fn (s, pos) =>
+        if member_string s ","
+        then error ("Single citation expected, without commas" ^ Position.here pos)
+        else ());
+    val citations' = space_implode "," (map #1 citations);
+    val markup = Markup.latex_cite {kind = kind, citations = citations'};
+  in [XML.Elem (markup, location)] end;
+
+
+(* index entries *)
+
+type index_item = {text: text, like: string};
+type index_entry = {items: index_item list, def: bool};
+
+fun index_item (item: index_item) =
+  XML.wrap_elem ((Markup.latex_index_item, #text item), XML.string (#like item));
+
+fun index_entry (entry: index_entry) =
+  [XML.Elem (Markup.latex_index_entry (if #def entry then "isaindexdef" else "isaindexref"),
+    map index_item (#items entry))];
+
+fun index_binding NONE = I
+  | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
+
+fun index_variants setup binding =
+  fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
+
+
+(* print mode *)
+
+val latexN = "latex";
+
+local
+
+fun latex_output str =
+  let val syms = Symbol.explode str
+  in (output_symbols syms, length_symbols syms) end;
+
+val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
+val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
+val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
+
+in
+
+fun latex_markup (s, _: Properties.T) =
+  if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup
+  else if s = Markup.keyword2N then keyword_markup
+  else Markup.no_output;
+
+val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
+val _ = Markup.add_mode latexN latex_markup;
+
+val _ = Pretty.add_mode latexN
+  (fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s);
+
+end;
+
+end;
diff -r c7a98469c0e7 -r c67b47cd41dc src/Pure/General/latex.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/latex.scala	Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,469 @@
+/*  Title:      Pure/General/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 {
+    enum Op { case fold, drop, keep }
+
+    val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
+
+    private def explode(spec: String): List[String] = space_explode(',', spec)
+
+    def apply(spec: String): Tags =
+      new Tags(spec,
+        (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op]) {
+          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]) {
+    override def toString: String = spec
+
+    def get(name: String): Option[Tags.Op] = 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}}}
+
+""" + 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_proper(item.like, 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_proper(entry.kind, "|" + 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).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 -r c7a98469c0e7 -r c67b47cd41dc src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jan 20 15:07:41 2024 +0100
+++ b/src/Pure/ROOT.ML	Sat Jan 20 16:09:35 2024 +0100
@@ -241,7 +241,7 @@
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_element.ML";
 ML_file "Thy/markdown.ML";
-ML_file "Thy/latex.ML";
+ML_file "General/latex.ML";
 
 (*ML with context and antiquotations*)
 ML_file "ML/ml_context.ML";
@@ -345,7 +345,7 @@
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
-ML_file "Thy/bibtex.ML";
+ML_file "General/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 
diff -r c7a98469c0e7 -r c67b47cd41dc src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(*  Title:      Pure/Thy/bibtex.ML
-    Author:     Makarius
-
-BibTeX support.
-*)
-
-signature BIBTEX =
-sig
-  val check_database:
-    Position.T -> string -> (string * Position.T) list * (string * Position.T) list
-  val check_database_output: Position.T -> string -> unit
-  val check_bibtex_entry: Proof.context -> string * Position.T -> unit
-  val cite_macro: string Config.T
-  val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
-end;
-
-structure Bibtex: BIBTEX =
-struct
-
-(* check database *)
-
-type message = string * Position.T;
-
-fun check_database pos0 database =
-  \<^scala>\<open>bibtex_check_database\<close> database
-  |> YXML.parse_body
-  |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
-  |> (apply2 o map o apsnd)
-      (fn pos => Position.of_properties (pos @ Position.properties_of pos0));
-
-fun check_database_output pos0 database =
-  let val (errors, warnings) = check_database pos0 database in
-    errors |> List.app (fn (msg, pos) =>
-      Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
-    warnings |> List.app (fn (msg, pos) =>
-      warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
-  end;
-
-
-(* check bibtex entry *)
-
-fun check_bibtex_entry ctxt (name, pos) =
-  let
-    fun warn () =
-      if Context_Position.is_visible ctxt then
-        warning ("Unknown session context: cannot check Bibtex entry " ^
-          quote name ^ Position.here pos)
-      else ();
-    fun decode yxml =
-      let
-        val props = XML.Decode.properties (YXML.parse_body yxml);
-        val name = Properties.get_string props Markup.nameN;
-        val pos = Position.of_properties props;
-      in (name, pos) end;
-  in
-    if name = "*" then ()
-    else
-      (case Position.id_of pos of
-        NONE => warn ()
-      | SOME id =>
-          (case \<^scala>\<open>bibtex_session_entries\<close> [id] of
-            [] => warn ()
-          | _ :: entries =>
-              Completion.check_entity Markup.bibtex_entryN (map decode entries)
-                ctxt (name, pos) |> ignore))
-  end;
-
-
-(* document antiquotations *)
-
-val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "");
-fun get_cite_macro ctxt = Config.get ctxt cite_macro;
-
-val _ =
-  Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro));
-
-
-local
-
-val parse_citations = Parse.and_list1 (Parse.position Parse.name);
-
-fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
-  let
-    val loc = the_default Input.empty opt_loc;
-    val _ = Context_Position.reports ctxt (Document_Output.document_reports loc);
-    val _ = List.app (check_bibtex_entry ctxt) citations;
-
-    val kind = if macro_name = "" then get_kind ctxt else macro_name;
-    val location = Document_Output.output_document ctxt {markdown = false} loc;
-  in Latex.cite {kind = kind, citations = citations, location = location} end;
-
-fun cite_command_old ctxt get_kind args =
-  let
-    val _ =
-      if Context_Position.is_visible ctxt then
-        legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^
-          Position.here_list (map snd (snd args)))
-      else ();
-  in cite_command ctxt get_kind (args, "") end;
-
-val cite_keywords =
-  Thy_Header.bootstrap_keywords
-  |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]);
-
-fun cite_command_embedded ctxt get_kind input =
-  let
-    val parser =
-      Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations --
-        Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) "";
-    val args = Parse.read_embedded ctxt cite_keywords parser input;
-  in cite_command ctxt get_kind args end;
-
-fun cite_command_parser get_kind =
-  Scan.option Args.cartouche_input -- parse_citations
-    >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) ||
-  Parse.embedded_input
-    >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);
-
-in
-
-fun cite_antiquotation binding get_kind =
-  Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind))
-    (fn ctxt => fn cmd => cmd ctxt);
-
-end;
-
-val _ =
-  Theory.setup
-   (cite_antiquotation \<^binding>\<open>cite\<close> get_cite_macro #>
-    cite_antiquotation \<^binding>\<open>nocite\<close> (K "nocite") #>
-    cite_antiquotation \<^binding>\<open>citet\<close> (K "citet") #>
-    cite_antiquotation \<^binding>\<open>citep\<close> (K "citep"));
-
-end;
diff -r c7a98469c0e7 -r c67b47cd41dc src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,855 +0,0 @@
-/*  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).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.capitalized(msg) + " in entry " + quote(name), chunk_pos(name))))
-              case (Warning(msg), Warning_Line(Value.Int(l))) =>
-                Some((false, (Word.capitalized(msg), get_line_pos(l))))
-              case (Warning(msg), _) =>
-                Some((false, (Word.capitalized(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(other.entries ::: entries, other.errors ::: 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.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_proper(title, " -h " + Bash.string(title) + " ") +
-          " " + 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] =
-    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_proper(location, 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 = 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 -r c7a98469c0e7 -r c67b47cd41dc src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(*  Title:      Pure/Thy/latex.ML
-    Author:     Makarius
-
-LaTeX output of theory sources.
-*)
-
-signature LATEX =
-sig
-  type text = XML.body
-  val text: string * Position.T -> text
-  val string: string -> text
-  val block: text -> XML.tree
-  val output: text -> text
-  val macro0: string -> text
-  val macro: string -> text -> text
-  val environment: string -> text -> text
-  val output_name: string -> string
-  val output_ascii: string -> string
-  val output_ascii_breakable: string -> string -> string
-  val output_symbols: Symbol.symbol list -> string
-  val output_syms: string -> string
-  val symbols: Symbol_Pos.T list -> text
-  val symbols_output: Symbol_Pos.T list -> text
-  val isabelle_body: string -> text -> text
-  val theory_entry: string -> string
-  val cite: {kind: string, citations: (string * Position.T) list, location: text} -> text
-  type index_item = {text: text, like: string}
-  type index_entry = {items: index_item list, def: bool}
-  val index_entry: index_entry -> text
-  val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
-  val latexN: string
-  val latex_markup: string * Properties.T -> Markup.output
-end;
-
-structure Latex: LATEX =
-struct
-
-(* text with positions *)
-
-type text = XML.body;
-
-fun text (s, pos) =
-  if s = "" then []
-  else if pos = Position.none then [XML.Text s]
-  else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
-
-fun string s = text (s, Position.none);
-
-fun block body = XML.Elem (Markup.document_latex, body);
-
-fun output body = [XML.Elem (Markup.latex_output, body)];
-
-fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
-fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
-fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
-
-
-(* output name for LaTeX macros *)
-
-val output_name =
-  translate_string
-    (fn "_" => "UNDERSCORE"
-      | "'" => "PRIME"
-      | "0" => "ZERO"
-      | "1" => "ONE"
-      | "2" => "TWO"
-      | "3" => "THREE"
-      | "4" => "FOUR"
-      | "5" => "FIVE"
-      | "6" => "SIX"
-      | "7" => "SEVEN"
-      | "8" => "EIGHT"
-      | "9" => "NINE"
-      | s => s);
-
-fun enclose_name bg en = enclose bg en o output_name;
-
-
-(* output verbatim ASCII *)
-
-val output_ascii =
-  translate_string
-    (fn " " => "\\ "
-      | "\t" => "\\ "
-      | "\n" => "\\isanewline\n"
-      | s =>
-          s
-          |> member_string "\"#$%&',-<>\\^_`{}~" s ? enclose "{\\char`\\" "}"
-          |> suffix "{\\kern0pt}");
-
-fun output_ascii_breakable sep =
-  space_explode sep
-  #> map output_ascii
-  #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
-
-
-(* output symbols *)
-
-local
-
-val char_table =
-  Symtab.make
-   [("\007", "{\\isacharbell}"),
-    ("!", "{\\isacharbang}"),
-    ("\"", "{\\isachardoublequote}"),
-    ("#", "{\\isacharhash}"),
-    ("$", "{\\isachardollar}"),
-    ("%", "{\\isacharpercent}"),
-    ("&", "{\\isacharampersand}"),
-    ("'", "{\\isacharprime}"),
-    ("(", "{\\isacharparenleft}"),
-    (")", "{\\isacharparenright}"),
-    ("*", "{\\isacharasterisk}"),
-    ("+", "{\\isacharplus}"),
-    (",", "{\\isacharcomma}"),
-    ("-", "{\\isacharminus}"),
-    (".", "{\\isachardot}"),
-    ("/", "{\\isacharslash}"),
-    (":", "{\\isacharcolon}"),
-    (";", "{\\isacharsemicolon}"),
-    ("<", "{\\isacharless}"),
-    ("=", "{\\isacharequal}"),
-    (">", "{\\isachargreater}"),
-    ("?", "{\\isacharquery}"),
-    ("@", "{\\isacharat}"),
-    ("[", "{\\isacharbrackleft}"),
-    ("\\", "{\\isacharbackslash}"),
-    ("]", "{\\isacharbrackright}"),
-    ("^", "{\\isacharcircum}"),
-    ("_", "{\\isacharunderscore}"),
-    ("`", "{\\isacharbackquote}"),
-    ("{", "{\\isacharbraceleft}"),
-    ("|", "{\\isacharbar}"),
-    ("}", "{\\isacharbraceright}"),
-    ("~", "{\\isachartilde}")];
-
-fun output_chr " " = "\\ "
-  | output_chr "\t" = "\\ "
-  | output_chr "\n" = "\\isanewline\n"
-  | output_chr c =
-      (case Symtab.lookup char_table c of
-        SOME s => s ^ "{\\kern0pt}"
-      | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
-
-fun output_sym sym =
-  (case Symbol.decode sym of
-    Symbol.Char s => output_chr s
-  | Symbol.UTF8 s => s
-  | Symbol.Sym s => enclose_name "{\\isasym" "}" s
-  | Symbol.Control s => enclose_name "\\isactrl" " " s
-  | Symbol.Malformed s => error (Symbol.malformed_msg s)
-  | Symbol.EOF => error "Bad EOF symbol");
-
-open Basic_Symbol_Pos;
-
-val scan_latex_length =
-  Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
-    >> (Symbol.length o map Symbol_Pos.symbol) ||
-  $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
-
-val scan_latex =
-  $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
-    >> (implode o map Symbol_Pos.symbol) ||
-  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
-
-fun read scan syms =
-  Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
-
-in
-
-val length_symbols =
-  Integer.build o fold Integer.add o these o read scan_latex_length;
-
-fun output_symbols syms =
-  if member (op =) syms Symbol.latex then
-    (case read scan_latex syms of
-      SOME ss => implode ss
-    | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
-  else implode (map output_sym syms);
-
-val output_syms = output_symbols o Symbol.explode;
-
-end;
-
-fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
-fun symbols_output syms =
-  text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
-
-
-(* theory presentation *)
-
-fun isabelle_body name =
-  XML.enclose
-   ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
-   "%\n\\end{isabellebody}%\n";
-
-fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
-
-
-(* cite: references to bibliography *)
-
-fun cite {kind, location, citations} =
-  let
-    val _ =
-      citations |> List.app (fn (s, pos) =>
-        if member_string s ","
-        then error ("Single citation expected, without commas" ^ Position.here pos)
-        else ());
-    val citations' = space_implode "," (map #1 citations);
-    val markup = Markup.latex_cite {kind = kind, citations = citations'};
-  in [XML.Elem (markup, location)] end;
-
-
-(* index entries *)
-
-type index_item = {text: text, like: string};
-type index_entry = {items: index_item list, def: bool};
-
-fun index_item (item: index_item) =
-  XML.wrap_elem ((Markup.latex_index_item, #text item), XML.string (#like item));
-
-fun index_entry (entry: index_entry) =
-  [XML.Elem (Markup.latex_index_entry (if #def entry then "isaindexdef" else "isaindexref"),
-    map index_item (#items entry))];
-
-fun index_binding NONE = I
-  | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
-
-fun index_variants setup binding =
-  fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
-
-
-(* print mode *)
-
-val latexN = "latex";
-
-local
-
-fun latex_output str =
-  let val syms = Symbol.explode str
-  in (output_symbols syms, length_symbols syms) end;
-
-val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
-val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
-val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
-
-in
-
-fun latex_markup (s, _: Properties.T) =
-  if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup
-  else if s = Markup.keyword2N then keyword_markup
-  else Markup.no_output;
-
-val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
-val _ = Markup.add_mode latexN latex_markup;
-
-val _ = Pretty.add_mode latexN
-  (fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s);
-
-end;
-
-end;
diff -r c7a98469c0e7 -r c67b47cd41dc src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,469 +0,0 @@
-/*  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 {
-    enum Op { case fold, drop, keep }
-
-    val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
-
-    private def explode(spec: String): List[String] = space_explode(',', spec)
-
-    def apply(spec: String): Tags =
-      new Tags(spec,
-        (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op]) {
-          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]) {
-    override def toString: String = spec
-
-    def get(name: String): Option[Tags.Op] = 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}}}
-
-""" + 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_proper(item.like, 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_proper(entry.kind, "|" + 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).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)
-  }
-}