src/Tools/jEdit/src/document_model.scala

   def get(buffer: JEditBuffer): Option[Buffer_Model] =
     state.value.buffer_models.get(buffer)
 
   def is_stable(): Boolean =
     state.value.models_iterator.forall(_.is_stable)
+
+  def bibtex_entries_iterator(): Iterator[(String, Document_Model, Text.Offset)] =
+    for {
+      model <- state.value.models_iterator
+      (entry, offset) <- model.bibtex_entries
+    } yield (entry, model, offset)
 
 
   /* init and exit */
 
   def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =

       try { Bibtex.parse_entries(text) }
       catch { case ERROR(msg) => Output.warning(msg); Nil }
   }
 }
 
-trait Document_Model extends Document.Model
+sealed abstract class Document_Model extends Document.Model
 {
   /* content */
 
   def bibtex_entries: List[(String, Text.Offset)]
 

     PIDE.resources.special_header(node_name) getOrElse
       PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
+
+  def node_position(offset: Text.Offset): Line.Node_Position =
+    Line.Node_Position(node_name.node,
+      Line.Position.zero.advance(content.text.substring(0, offset), Text.Length))
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))