clarified signature: internalize errors (but: the parser rarely fails);

--- a/src/Pure/Thy/bibtex.scala	Mon Dec 26 15:24:57 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala	Mon Dec 26 16:44:13 2022 +0100
@@ -157,34 +157,36 @@
   object Entries {
     val empty: Entries = apply(Nil)
 
-    def apply(entries: List[Text.Info[String]]): Entries = new Entries(entries)
+    def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries =
+      new Entries(entries, errors)
 
     def parse(text: String): Entries = {
-      val result = new mutable.ListBuffer[Text.Info[String]]
+      val entries = new mutable.ListBuffer[Text.Info[String]]
       var offset = 0
-      for (chunk <- Bibtex.parse(text)) {
-        val end_offset = offset + chunk.source.length
-        if (chunk.name != "" && !chunk.is_command)
-          result += Text.Info(Text.Range(offset, end_offset), chunk.name)
-        offset = end_offset
+
+      try {
+        for (chunk <- Bibtex.parse(text)) {
+          val end_offset = offset + chunk.source.length
+          if (chunk.name != "" && !chunk.is_command) {
+            entries += Text.Info(Text.Range(offset, end_offset), chunk.name)
+          }
+          offset = end_offset
+        }
+        apply(entries.toList)
       }
-      apply(result.toList)
+      catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
     }
 
-    def try_parse(text: String): Entries =
-      try { parse(text) }
-      catch { case ERROR(_) => empty }
-
     def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] =
       for {
         model <- models.iterator
-        info <- model.bibtex_entries
+        info <- model.bibtex_entries.entries.iterator
       } yield info.map((_, model))
   }
 
-  final class Entries private(val entries: List[Text.Info[String]])
-  extends Iterable[Text.Info[String]] {
-    def iterator: Iterator[Text.Info[String]] = entries.iterator
+  final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
+    def ::: (other: Entries): Entries =
+      new Entries(entries ::: other.entries, errors ::: other.errors)
   }
 
 

--- a/src/Pure/Thy/sessions.scala	Mon Dec 26 15:24:57 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 26 16:44:13 2022 +0100
@@ -439,9 +439,7 @@
               try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
               catch { case ERROR(msg) => List(msg) }
 
-            val bibtex_errors =
-              try { info.bibtex_entries; Nil }
-              catch { case ERROR(msg) => List(msg) }
+            val bibtex_errors = info.bibtex_entries.errors
 
             val base =
               Base(
@@ -640,12 +638,13 @@
     def browser_info: Boolean = options.bool("browser_info")
 
     lazy val bibtex_entries: Bibtex.Entries =
-      Bibtex.Entries(
-        (for {
-          (document_dir, file) <- document_files.iterator
-          if File.is_bib(file.file_name)
-          info <- Bibtex.Entries.parse(File.read(dir + document_dir + file)).iterator
-        } yield info).toList)
+      (for {
+        (document_dir, file) <- document_files.iterator
+        if File.is_bib(file.file_name)
+      } yield {
+        val path = dir + document_dir + file
+        Bibtex.Entries.parse(File.read(path))
+      }).foldRight(Bibtex.Entries.empty)(_ ::: _)
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 

--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 15:24:57 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 16:44:13 2022 +0100
@@ -38,7 +38,7 @@
 
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.try_parse(text)
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text)
 
     def recode_symbols: List[LSP.TextEdit] =
       (for {

--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 15:24:57 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 16:44:13 2022 +0100
@@ -291,7 +291,7 @@
   sealed case class File_Content(text: String) {
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.try_parse(text)
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text)
   }
 
 
@@ -595,9 +595,8 @@
       if (File.is_bib(node_name.node)) {
         bibtex_entries getOrElse {
           val text = JEdit_Lib.buffer_text(buffer)
-          val entries =
-            try { Bibtex.Entries.parse(text) }
-            catch { case ERROR(msg) => Output.warning(msg); Bibtex.Entries.empty }
+          val entries = Bibtex.Entries.parse(text)
+          if (entries.errors.nonEmpty) Output.warning(cat_lines(entries.errors))
           bibtex_entries = Some(entries)
           entries
         }