--- a/src/Pure/PIDE/editor.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Pure/PIDE/editor.scala Tue Dec 27 22:48:01 2022 +0100
@@ -8,12 +8,24 @@
abstract class Editor[Context] {
- /* session */
+ /* PIDE session and document model */
def session: Session
def flush(): Unit
def invoke(): Unit
+ def get_models(): Iterable[Document.Model]
+
+
+ /* bibtex */
+
+ def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document.Model)]] =
+ Bibtex.Entries.iterator(get_models())
+
+ def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
+ : Option[Completion.Result] =
+ Bibtex.completion(history, rendering, caret, get_models())
+
/* document editor */
--- a/src/Tools/VSCode/src/language_server.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Tue Dec 27 22:48:01 2022 +0100
@@ -480,12 +480,14 @@
/* abstract editor operations */
object editor extends Language_Server.Editor {
- /* session */
+ /* PIDE session and document model */
override def session: Session = server.session
override def flush(): Unit = resources.flush_input(session, channel)
override def invoke(): Unit = delay_input.invoke()
+ override def get_models(): Iterable[Document.Model] = resources.get_models()
+
/* current situation */
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Dec 27 22:48:01 2022 +0100
@@ -75,15 +75,6 @@
override def get_text(range: Text.Range): Option[String] = model.get_text(range)
- /* bibtex */
-
- def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_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(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
@@ -114,7 +105,7 @@
syntax_completion,
VSCode_Spell_Checker.completion(rendering, caret),
path_completion(caret),
- bibtex_completion(history, caret))
+ model.editor.bibtex_completion(history, rendering, caret))
val items =
results match {
case None => Nil
@@ -323,7 +314,8 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val iterator =
for {
- Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator()
+ Text.Info(entry_range, (entry, model: VSCode_Model)) <-
+ model.editor.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(iterator.foldLeft(links)(_ :+ _))
--- a/src/Tools/jEdit/src/completion_popup.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Dec 27 22:48:01 2022 +0100
@@ -122,7 +122,7 @@
Completion.Result.merge(Completion.History.empty,
syntax_completion(Completion.History.empty, true, Some(rendering)),
rendering.path_completion(caret),
- Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
+ PIDE.editor.bibtex_completion(Completion.History.empty, rendering, caret))
.map(_.range)
rendering.semantic_completion(range0, range) match {
case None => range0
@@ -304,7 +304,7 @@
result1,
JEdit_Spell_Checker.completion(rendering, explicit, caret),
rendering.path_completion(caret),
- Document_Model.bibtex_completion(history, rendering, caret))
+ PIDE.editor.bibtex_completion(history, rendering, caret))
}
}
result match {
--- a/src/Tools/jEdit/src/document_model.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 27 22:48:01 2022 +0100
@@ -100,16 +100,6 @@
def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot)
- /* bibtex */
-
- def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
- Bibtex.Entries.iterator(get_models())
-
- def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
- : Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, get_models())
-
-
/* overlays */
def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Dec 27 22:48:01 2022 +0100
@@ -18,7 +18,7 @@
class JEdit_Editor extends Editor[View] {
- /* session */
+ /* PIDE session and document model */
override def session: Session = PIDE.session
@@ -53,6 +53,9 @@
} yield doc_view.model.node_name).contains(name)
+ override def get_models(): Iterable[Document.Model] = Document_Model.get_models()
+
+
/* global changes */
def state_changed(): Unit = {
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Dec 27 22:08:31 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Dec 27 22:48:01 2022 +0100
@@ -272,8 +272,8 @@
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val opt_link =
- Document_Model.bibtex_entries_iterator().collectFirst(
- { case Text.Info(entry_range, (entry, model)) if entry == name =>
+ PIDE.editor.bibtex_entries_iterator().collectFirst(
+ { case Text.Info(entry_range, (entry, model: Document_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))