src/Tools/jEdit/src/document_model.scala
changeset 64829 07f209e957bc
parent 64828 e837f6bf653c
child 64831 4792ee012e94
--- a/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 10:56:33 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Jan 08 11:41:18 2017 +0100
@@ -77,6 +77,12 @@
   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 */
 
@@ -193,7 +199,7 @@
   }
 }
 
-trait Document_Model extends Document.Model
+sealed abstract class Document_Model extends Document.Model
 {
   /* content */
 
@@ -245,6 +251,10 @@
 
   /* 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))