# HG changeset patch
# User wenzelm
# Date 1672063902 -3600
# Node ID 011759a7f2f68a80383f29731d5946a3271cc713
# Parent  01a7265db76b0301774cf6b74c5f1cc5a2c0a3a1
clarified signature: more explicit types;

diff -r 01a7265db76b -r 011759a7f2f6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Dec 26 12:33:55 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Dec 26 15:11:42 2022 +0100
@@ -796,7 +796,7 @@
     def node_required: Boolean
 
     def get_blob: Option[Blob]
-    def bibtex_entries: List[Text.Info[String]]
+    def bibtex_entries: Bibtex.Entries
 
     def node_edits(
       node_header: Node.Header,
diff -r 01a7265db76b -r 011759a7f2f6 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Mon Dec 26 12:33:55 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala	Mon Dec 26 15:11:42 2022 +0100
@@ -154,35 +154,47 @@
 
   /* entries */
 
-  def entries(text: String): List[Text.Info[String]] = {
-    val result = new mutable.ListBuffer[Text.Info[String]]
-    var offset = 0
-    for (chunk <- Bibtex.parse(text)) {
-      val end_offset = offset + chunk.source.length
-      if (chunk.name != "" && !chunk.is_command)
-        result += Text.Info(Text.Range(offset, end_offset), chunk.name)
-      offset = end_offset
+  object Entries {
+    val empty: Entries = apply(Nil)
+
+    def apply(entries: List[Text.Info[String]]): Entries = new Entries(entries)
+
+    def parse(text: String): Entries = {
+      val result = new mutable.ListBuffer[Text.Info[String]]
+      var offset = 0
+      for (chunk <- Bibtex.parse(text)) {
+        val end_offset = offset + chunk.source.length
+        if (chunk.name != "" && !chunk.is_command)
+          result += Text.Info(Text.Range(offset, end_offset), chunk.name)
+        offset = end_offset
+      }
+      apply(result.toList)
     }
-    result.toList
+
+    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
+      } yield info.map((_, model))
   }
 
-  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))
+  final class Entries private(val entries: List[Text.Info[String]])
+  extends Iterable[Text.Info[String]] {
+    def iterator: Iterator[Text.Info[String]] = entries.iterator
   }
 
 
   /* completion */
 
-  def completion[A, B <: Document.Model](
+  def completion[A <: Document.Model](
     history: Completion.History,
     rendering: Rendering,
     caret: Text.Offset,
-    models: Map[A, B]
+    models: Iterable[A]
   ): Option[Completion.Result] = {
     for {
       Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
@@ -193,7 +205,7 @@
 
       entries =
         (for {
-          Text.Info(_, (entry, _)) <- entries_iterator(models)
+          Text.Info(_, (entry, _)) <- Entries.iterator(models)
           if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
         } yield entry).toList
       if entries.nonEmpty
diff -r 01a7265db76b -r 011759a7f2f6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 26 12:33:55 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 26 15:11:42 2022 +0100
@@ -639,12 +639,13 @@
 
     def browser_info: Boolean = options.bool("browser_info")
 
-    lazy val bibtex_entries: List[Text.Info[String]] =
-      (for {
-        (document_dir, file) <- document_files.iterator
-        if File.is_bib(file.file_name)
-        info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
-      } yield info).toList
+    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)
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 
@@ -923,11 +924,12 @@
     def imports_topological_order: List[String] = imports_graph.topological_order
 
     def bibtex_entries: List[(String, List[String])] =
-      build_topological_order.flatMap(name =>
-        apply(name).bibtex_entries match {
+      build_topological_order.flatMap { name =>
+        apply(name).bibtex_entries.entries match {
           case Nil => None
           case entries => Some(name -> entries.map(_.info))
-        })
+        }
+      }
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
diff -r 01a7265db76b -r 011759a7f2f6 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 12:33:55 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 15:11:42 2022 +0100
@@ -38,9 +38,7 @@
 
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: List[Text.Info[String]] =
-      try { Bibtex.entries(text) }
-      catch { case ERROR(_) => Nil }
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.try_parse(text)
 
     def recode_symbols: List[LSP.TextEdit] =
       (for {
@@ -153,8 +151,7 @@
 
   /* bibtex entries */
 
-  def bibtex_entries: List[Text.Info[String]] =
-    model.content.bibtex_entries
+  def bibtex_entries: Bibtex.Entries = model.content.bibtex_entries
 
 
   /* edits */
diff -r 01a7265db76b -r 011759a7f2f6 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Dec 26 12:33:55 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Dec 26 15:11:42 2022 +0100
@@ -78,10 +78,10 @@
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] =
-    Bibtex.entries_iterator(resources.get_models())
+    Bibtex.Entries.iterator(resources.get_models().values)
 
   def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
-    Bibtex.completion(history, rendering, caret, resources.get_models())
+    Bibtex.completion(history, rendering, caret, resources.get_models().values)
 
 
   /* completion */
diff -r 01a7265db76b -r 011759a7f2f6 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 12:33:55 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 15:11:42 2022 +0100
@@ -101,11 +101,11 @@
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
-    Bibtex.entries_iterator(state.value.models)
+    Bibtex.Entries.iterator(get_models().values)
 
   def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
       : Option[Completion.Result] =
-    Bibtex.completion(history, rendering, caret, state.value.models)
+    Bibtex.completion(history, rendering, caret, get_models().values)
 
 
   /* overlays */
@@ -290,9 +290,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: List[Text.Info[String]] =
-      try { Bibtex.entries(text) }
-      catch { case ERROR(_) => Nil }
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.try_parse(text)
   }
 
 
@@ -441,8 +439,8 @@
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
-  def bibtex_entries: List[Text.Info[String]] =
-    if (File.is_bib(node_name.node)) content.bibtex_entries else Nil
+  def bibtex_entries: Bibtex.Entries =
+    if (File.is_bib(node_name.node)) content.bibtex_entries else Bibtex.Entries.empty
 
 
   /* edits */
@@ -588,22 +586,22 @@
 
     // bibtex entries
 
-    private var bibtex_entries: Option[List[Text.Info[String]]] = None
+    private var bibtex_entries: Option[Bibtex.Entries] = None
 
     def reset_bibtex_entries(): Unit = GUI_Thread.require { bibtex_entries = None }
 
-    def get_bibtex_entries: List[Text.Info[String]] = GUI_Thread.require {
+    def get_bibtex_entries: Bibtex.Entries = GUI_Thread.require {
       if (File.is_bib(node_name.node)) {
         bibtex_entries getOrElse {
           val text = JEdit_Lib.buffer_text(buffer)
           val entries =
-            try { Bibtex.entries(text) }
-            catch { case ERROR(msg) => Output.warning(msg); Nil }
+            try { Bibtex.Entries.parse(text) }
+            catch { case ERROR(msg) => Output.warning(msg); Bibtex.Entries.empty }
           bibtex_entries = Some(entries)
           entries
         }
       }
-      else Nil
+      else Bibtex.Entries.empty
     }
   }
 
@@ -617,7 +615,7 @@
 
   def get_blob: Option[Document.Blob] = buffer_state.get_blob
 
-  def bibtex_entries: List[Text.Info[String]] = buffer_state.get_bibtex_entries
+  def bibtex_entries: Bibtex.Entries = buffer_state.get_bibtex_entries
 
 
   /* buffer listener */