src/Pure/Thy/bibtex.scala

 import scala.collection.mutable
 import scala.util.parsing.combinator.RegexParsers
 import scala.util.parsing.input.Reader
 
 
-object Bibtex
-{
+object Bibtex {
   /** file format **/
 
   def is_bibtex(name: String): Boolean = name.endsWith(".bib")
 
-  class File_Format extends isabelle.File_Format
-  {
+  class File_Format extends isabelle.File_Format {
     val format_name: String = "bibtex"
     val file_ext: String = "bib"
 
     override def theory_suffix: String = "bibtex_file"
     override def theory_content(name: String): String =
       """theory "bib" imports Pure begin bibtex_file """ +
         Outer_Syntax.quote_string(name) + """ end"""
 
-    override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
-    {
+    override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = {
       val name = snapshot.node_name
       if (detect(name.node)) {
         val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>

 
 
 
   /** bibtex errors **/
 
-  def bibtex_errors(dir: Path, root_name: String): List[String] =
-  {
+  def bibtex_errors(dir: Path, root_name: String): List[String] = {
     val log_path = dir + Path.explode(root_name).ext("blg")
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
       val Error2 = """^(I found no .+)$""".r
       val Error3 = """^(.+)---line (\d+) of file (.+)""".r

 
 
 
   /** check database **/
 
-  def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) =
-  {
+  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 =
-    {
+    def advance_pos(tok: Token): Unit = {
       for (s <- Symbol.iterator(tok.source)) {
         if (Symbol.is_newline(s)) line += 1
         offset += 1
       }
     }

         tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
         advance_pos(tok)
       }
     }
 
-    Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
-    {
+    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)

         }
       (errors.map(_._2), warnings.map(_._2))
     })
   }
 
-  object Check_Database extends Scala.Fun_String("bibtex_check_database")
-  {
+  object Check_Database extends Scala.Fun_String("bibtex_check_database") {
     val here = Scala_Project.here
-    def apply(database: String): String =
-    {
+    def apply(database: String): String = {
       import XML.Encode._
       YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
         check_database(database)))
     }
   }

 
   /** document model **/
 
   /* entries */
 
-  def entries(text: String): List[Text.Info[String]] =
-  {
+  def entries(text: String): List[Text.Info[String]] = {
     val result = new mutable.ListBuffer[Text.Info[String]]
     var offset = 0
     for (chunk <- Bibtex.parse(text)) {
       val end_offset = offset + chunk.source.length
       if (chunk.name != "" && !chunk.is_command)

       offset = end_offset
     }
     result.toList
   }
 
-  def entries_iterator[A, B <: Document.Model](models: Map[A, B])
-    : Iterator[Text.Info[(String, B)]] =
-  {
+  def entries_iterator[A, B <: Document.Model](
+    models: Map[A, B]
+  ): Iterator[Text.Info[(String, B)]] = {
     for {
       (_, model) <- models.iterator
       info <- model.bibtex_entries.iterator
     } yield info.map((_, model))
   }
 
 
   /* completion */
 
   def completion[A, B <: Document.Model](
-    history: Completion.History, rendering: Rendering, caret: Text.Offset,
-    models: Map[A, B]): Option[Completion.Result] =
-  {
+    history: Completion.History,
+    rendering: Rendering,
+    caret: Text.Offset,
+    models: Map[A, B]
+  ): Option[Completion.Result] = {
     for {
       Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
       name1 <- Completion.clean_name(name)
 
       original <- rendering.get_text(r)

 
   sealed case class Entry(
     kind: String,
     required: List[String],
     optional_crossref: List[String],
-    optional_other: 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) ||

 
 
 
   /** tokens and chunks **/
 
-  object Token
-  {
-    object Kind extends Enumeration
-    {
+  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 COMMENT = Value("ignored text")
       val ERROR = Value("bad input")
     }
   }
 
-  sealed case class Token(kind: Token.Kind.Value, source: String)
-  {
+  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.ERROR
     def is_open: Boolean =
       kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
   }
 
-  case class Chunk(kind: String, tokens: List[Token])
-  {
+  case class Chunk(kind: String, tokens: List[Token]) {
     val source = tokens.map(_.source).mkString
 
     private val content: Option[List[Token]] =
       tokens match {
         case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>

 
 
   // 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
-  {
+  object Parsers extends RegexParsers {
     /* white space and comments */
 
     override val whiteSpace = "".r
 
     private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)

 
     /* 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)]
-      {
+      new Parser[(String, Delimited)] {
         require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
           "bad delimiter depth")
 
-        def apply(in: Input) =
-        {
+        def apply(in: Input) = {
           val start = in.offset
           val end = in.source.length
 
           var i = start
           var q = delim.quoted

 
     /* chunks */
 
     val chunk: Parser[Chunk] = ignored | (item | recover_item)
 
-    def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] =
-    {
+    def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = {
       ctxt match {
         case Ignored =>
           ignored_line |
           at ^^ { case a => (Chunk("", List(a)), At) }
 

     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) =
-  {
+  def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = {
     var in: Reader[Char] = Scan.char_reader(input)
     val chunks = new mutable.ListBuffer[Chunk]
     var ctxt = context
     while (!in.atEnd) {
       Parsers.parse(Parsers.chunk_line(ctxt), in) match {

   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 =>
-    {
+    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 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 })
       }