# HG changeset patch # User wenzelm # Date 1672177681 -3600 # Node ID 941d4f5270916b75178551b91056c78405598fee # Parent fa70b536ec500865667ca1a8402891c6a56a4288 clarified modules: avoid duplication; diff -r fa70b536ec50 -r 941d4f527091 src/Pure/PIDE/editor.scala --- 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 */ diff -r fa70b536ec50 -r 941d4f527091 src/Tools/VSCode/src/language_server.scala --- 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 */ diff -r fa70b536ec50 -r 941d4f527091 src/Tools/VSCode/src/vscode_rendering.scala --- 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)(_ :+ _)) diff -r fa70b536ec50 -r 941d4f527091 src/Tools/jEdit/src/completion_popup.scala --- 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 { diff -r fa70b536ec50 -r 941d4f527091 src/Tools/jEdit/src/document_model.scala --- 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 = diff -r fa70b536ec50 -r 941d4f527091 src/Tools/jEdit/src/jedit_editor.scala --- 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 = { diff -r fa70b536ec50 -r 941d4f527091 src/Tools/jEdit/src/jedit_rendering.scala --- 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))