src/Pure/PIDE/editor.scala
changeset 76794 941d4f527091
parent 76739 cb72b5996520
child 77029 1046a69fabaa
--- 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 */