--- 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))