--- 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)
- }
}
--- 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)(_ :+ _))
--- 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)
--- 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 {
--- 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 */
--- 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] =