# HG changeset patch
# User wenzelm
# Date 1498046776 -7200
# Node ID c2e19b9e13989869273e9eb2fe28bdd8285097ab
# Parent  4bf16fb7c14d84cb9c54d30a9e288b839beb1967
tuned signature;

diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -502,6 +502,7 @@
 
     def node_required: Boolean
     def get_blob: Option[Blob]
+    def bibtex_entries: List[Text.Info[String]]
 
     def node_edits(
       node_header: Node.Header,
diff -r 4bf16fb7c14d -r c2e19b9e1398 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
 
diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -43,7 +43,7 @@
     lazy val bytes: Bytes = Bytes(text)
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
-      try { Bibtex.document_entries(text) }
+      try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
   }
 
@@ -133,6 +133,12 @@
     else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)))
 
 
+  /* bibtex entries */
+
+  def bibtex_entries: List[Text.Info[String]] =
+    model.content.bibtex_entries
+
+
   /* edits */
 
   def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] =
diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -303,7 +303,7 @@
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val iterator =
               for {
-                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
+                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator()
                 if entry == name
               } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
             if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -129,10 +129,7 @@
     }
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
-    for {
-      (_, model) <- state.value.models.iterator
-      info <- model.content.bibtex_entries.iterator
-    } yield info.map((_, model))
+    Bibtex.entries_iterator(state.value.models)
 
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -78,10 +78,7 @@
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
-    for {
-      (_, model) <- state.value.models.iterator
-      info <- model.bibtex_entries.iterator
-    } yield info.map((_, model))
+    Bibtex.entries_iterator(state.value.models)
 
 
   /* overlays */
@@ -275,7 +272,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.document_entries(text) }
+      try { Bibtex.entries(text) }
       catch { case ERROR(msg) => Output.warning(msg); Nil }
   }
 
@@ -551,7 +548,7 @@
           case None =>
             val text = JEdit_Lib.buffer_text(buffer)
             val entries =
-              try { Bibtex.document_entries(text) }
+              try { Bibtex.entries(text) }
               catch { case ERROR(msg) => Output.warning(msg); Nil }
             _bibtex_entries = Some(entries)
             entries
diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -50,7 +50,7 @@
           case buffer: Buffer
           if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
             val menu = new JMenu("BibTeX entries")
-            for (entry <- Bibtex.entries) {
+            for (entry <- Bibtex.known_entries) {
               val item = new JMenuItem(entry.kind)
               item.addActionListener(new ActionListener {
                 def actionPerformed(evt: ActionEvent): Unit =
diff -r 4bf16fb7c14d -r c2e19b9e1398 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jun 20 13:07:49 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Jun 21 14:06:16 2017 +0200
@@ -259,7 +259,7 @@
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val opt_link =
-              Document_Model.bibtex_entries_iterator.collectFirst(
+              Document_Model.bibtex_entries_iterator().collectFirst(
                 { case Text.Info(entry_range, (entry, model)) if entry == name =>
                     PIDE.editor.hyperlink_model(true, model, entry_range.start) })
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))