src/Pure/Tools/bibtex.scala

--- a/src/Pure/Tools/bibtex.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Pure/Tools/bibtex.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -19,7 +19,7 @@
   def check_name(name: String): Boolean = name.endsWith(".bib")
   def check_name(name: Document.Node.Name): Boolean = check_name(name.node)
 
-  def document_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
@@ -32,6 +32,15 @@
     result.toList
   }
 
+  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))
+  }
+
 
 
   /** content **/
@@ -69,7 +78,7 @@
       "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
   }
 
-  val entries: List[Entry] =
+  val known_entries: List[Entry] =
     List(
       Entry("Article",
         List("author", "title"),
@@ -128,7 +137,7 @@
         List("author", "title", "howpublished", "month", "year", "note")))
 
   def get_entry(kind: String): Option[Entry] =
-    entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
+    known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
 
   def is_entry(kind: String): Boolean = get_entry(kind).isDefined