# HG changeset patch
# User wenzelm
# Date 1498049804 -7200
# Node ID 18e1aba549f6235cab01626ebf675299df68856f
# Parent  26eecd42cbc5aa3ba77c24fcfa691c97b75ec594
tuned signature;

diff -r 26eecd42cbc5 -r 18e1aba549f6 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Wed Jun 21 14:30:20 2017 +0200
+++ b/src/Pure/Tools/bibtex.scala	Wed Jun 21 14:56:44 2017 +0200
@@ -42,6 +42,38 @@
   }
 
 
+  /* completion */
+
+  def completion[A, B <: Document.Model](
+    history: Completion.History, rendering: Rendering, caret: Text.Offset,
+    models: Map[A, B]): Option[Completion.Result] =
+  {
+    for {
+      Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
+      name1 <- Completion.clean_name(name)
+
+      original <- rendering.model.try_get_text(r)
+      original1 <- Completion.clean_name(Library.perhaps_unquote(original))
+
+      entries =
+        (for {
+          Text.Info(_, (entry, _)) <- entries_iterator(models)
+          if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
+        } yield entry).toList
+      if entries.nonEmpty
+
+      items =
+        entries.sorted.map({
+          case entry =>
+            val full_name = Long_Name.qualify(Markup.CITATION, entry)
+            val description = List(entry, "(BibTeX entry)")
+            val replacement = quote(entry)
+          Completion.Item(r, original, full_name, description, replacement, 0, false)
+        }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
+    } yield Completion.Result(r, original, false, items)
+  }
+
+
 
   /** content **/
 
@@ -431,31 +463,4 @@
     }
     (chunks.toList, ctxt)
   }
-
-
-  /* completion */
-
-  def completion(history: Completion.History, rendering: Rendering, caret: Text.Offset,
-    complete: String => List[String]): Option[Completion.Result] =
-  {
-    for {
-      Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
-      name1 <- Completion.clean_name(name)
-
-      original <- rendering.model.try_get_text(r)
-      original1 <- Completion.clean_name(Library.perhaps_unquote(original))
-
-      entries = complete(name1).filter(_ != original1)
-      if entries.nonEmpty
-
-      items =
-        entries.sorted.map({
-          case entry =>
-            val full_name = Long_Name.qualify(Markup.CITATION, entry)
-            val description = List(entry, "(BibTeX entry)")
-            val replacement = quote(entry)
-          Completion.Item(r, original, full_name, description, replacement, 0, false)
-        }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
-    } yield Completion.Result(r, original, false, items)
-  }
 }
diff -r 26eecd42cbc5 -r 18e1aba549f6 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:30:20 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:56:44 2017 +0200
@@ -74,6 +74,15 @@
   def resources: VSCode_Resources = model.resources
 
 
+  /* bibtex */
+
+  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
+    Bibtex.entries_iterator(resources.get_models)
+
+  def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
+    Bibtex.completion(history, rendering, caret, resources.get_models)
+
+
   /* completion */
 
   def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
@@ -304,7 +313,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)) <- 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 26eecd42cbc5 -r 18e1aba549f6 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Jun 21 14:30:20 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Jun 21 14:56:44 2017 +0200
@@ -112,7 +112,8 @@
     else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
   }
 
-  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
+  def get_models: Map[JFile, Document_Model] = state.value.models
+  def get_model(file: JFile): Option[Document_Model] = get_models.get(file)
   def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
 
 
@@ -128,9 +129,6 @@
       case None => read_file_content(file)
     }
 
-  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
-    Bibtex.entries_iterator(state.value.models)
-
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val file = node_file(name)
diff -r 26eecd42cbc5 -r 18e1aba549f6 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 14:30:20 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 14:56:44 2017 +0200
@@ -133,7 +133,7 @@
                   Completion.Result.merges(Completion.History.empty,
                     syntax_completion(Completion.History.empty, true, Some(rendering)),
                     path_completion(rendering),
-                    JEdit_Bibtex.completion(Completion.History.empty, rendering, caret))
+                    Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
                   .map(_.range)
                 rendering.semantic_completion(range0, range) match {
                   case None => range0
@@ -375,7 +375,7 @@
                   result1,
                   JEdit_Spell_Checker.completion(rendering, explicit, caret),
                   path_completion(rendering),
-                  JEdit_Bibtex.completion(history, rendering, caret))
+                  Document_Model.bibtex_completion(history, rendering, caret))
             }
           }
           result match {
diff -r 26eecd42cbc5 -r 18e1aba549f6 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 21 14:30:20 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 21 14:56:44 2017 +0200
@@ -77,9 +77,16 @@
   def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
+
+  /* bibtex */
+
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     Bibtex.entries_iterator(state.value.models)
 
+  def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
+      : Option[Completion.Result] =
+    Bibtex.completion(history, rendering, caret, state.value.models)
+
 
   /* overlays */
 
diff -r 26eecd42cbc5 -r 18e1aba549f6 src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Wed Jun 21 14:30:20 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Wed Jun 21 14:56:44 2017 +0200
@@ -27,19 +27,6 @@
 
 object JEdit_Bibtex
 {
-  /** completion **/
-
-  def complete(name: String): List[String] =
-    (for {
-      Text.Info(_, (entry, _)) <- Document_Model.bibtex_entries_iterator()
-      if entry.toLowerCase.containsSlice(name.toLowerCase)
-    } yield entry).toList
-
-  def completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
-    : Option[Completion.Result] = Bibtex.completion(history, rendering, caret, complete _)
-
-
-
   /** context menu **/
 
   def context_menu(text_area0: JEditTextArea): List[JMenuItem] =