clarified signature: more position information via node_name;

--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 17:36:56 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 18:41:27 2022 +0100
@@ -26,11 +26,7 @@
 
   /* content */
 
-  object Content {
-    val empty: Content = Content(Line.Document.empty)
-  }
-
-  sealed case class Content(doc: Line.Document) {
+  sealed case class Content(node_name: Document.Node.Name, doc: Line.Document) {
     override def toString: String = doc.toString
     def text_length: Text.Offset = doc.text_length
     def text_range: Text.Range = doc.text_range
@@ -38,7 +34,7 @@
 
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text)
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
 
     def recode_symbols: List[LSP.TextEdit] =
       (for {
@@ -56,15 +52,15 @@
     editor: Language_Server.Editor,
     node_name: Document.Node.Name
   ): VSCode_Model = {
-    VSCode_Model(session, editor, node_name, Content.empty,
-      node_required = File_Format.registry.is_theory(node_name))
+    val content = Content(node_name, Line.Document.empty)
+    val is_theory = File_Format.registry.is_theory(node_name)
+    VSCode_Model(session, editor, content, node_required = is_theory)
   }
 }
 
 sealed case class VSCode_Model(
   session: Session,
   editor: Language_Server.Editor,
-  node_name: Document.Node.Name,
   content: VSCode_Model.Content,
   version: Option[Long] = None,
   external_file: Boolean = false,
@@ -79,6 +75,8 @@
 
   /* content */
 
+  def node_name: Document.Node.Name = content.node_name
+
   def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
 
   def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version))
@@ -163,7 +161,7 @@
         Text.Edit.replace(0, content.text, insert) match {
           case Nil => None
           case edits =>
-            val content1 = VSCode_Model.Content(Line.Document(insert))
+            val content1 = VSCode_Model.Content(node_name, Line.Document(insert))
             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
         }
       case Some(remove) =>
@@ -171,7 +169,7 @@
           case None => error("Failed to apply document change: " + remove)
           case Some((Nil, _)) => None
           case Some((edits, doc1)) =>
-            val content1 = VSCode_Model.Content(doc1)
+            val content1 = VSCode_Model.Content(node_name, doc1)
             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
         }
     }

--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 17:36:56 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 18:41:27 2022 +0100
@@ -132,7 +132,7 @@
           text <- PIDE.resources.read_file_content(node_name)
           if model.content.text != text
         } yield {
-          val content = Document_Model.File_Content(text)
+          val content = Document_Model.File_Content(node_name, text)
           val edits = Text.Edit.replace(0, model.content.text, text)
           (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
         }).toList
@@ -288,10 +288,18 @@
 
   /* file content */
 
-  sealed case class File_Content(text: String) {
+  object File_Content {
+    val empty: File_Content = apply(Document.Node.Name.empty, "")
+
+    def apply(node_name: Document.Node.Name, text: String): File_Content =
+      new File_Content(node_name, text)
+  }
+
+  final class File_Content private(val node_name: Document.Node.Name, val text: String) {
+    override def toString: String = "Document_Model.File_Content(" + node_name.node + ")"
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text)
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
   }
 
 
@@ -384,7 +392,7 @@
 
 object File_Model {
   def empty(session: Session): File_Model =
-    File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
+    File_Model(session, None, Document_Model.File_Content.empty,
       false, Document.Node.Perspective_Text.empty, Nil)
 
   def init(session: Session,
@@ -397,32 +405,33 @@
     val file = JEdit_Lib.check_file(node_name.node)
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
-    val content = Document_Model.File_Content(text)
+    val content = Document_Model.File_Content(node_name, text)
     val node_required1 = node_required || File_Format.registry.is_theory(node_name)
-    File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
+    File_Model(session, file, content, node_required1, last_perspective, pending_edits)
   }
 }
 
 case class File_Model(
   session: Session,
-  node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
   node_required: Boolean,
   last_perspective: Document.Node.Perspective_Text.T,
   pending_edits: List[Text.Edit]
 ) extends Document_Model {
+  /* content */
+
+  def node_name: Document.Node.Name = content.node_name
+
+  def get_text(range: Text.Range): Option[String] =
+    range.try_substring(content.text)
+
+
   /* required */
 
   def set_node_required(b: Boolean): File_Model = copy(node_required = b)
 
 
-  /* text */
-
-  def get_text(range: Text.Range): Option[String] =
-    range.try_substring(content.text)
-
-
   /* header */
 
   def node_header: Document.Node.Header =
@@ -450,7 +459,7 @@
     Text.Edit.replace(0, content.text, text) match {
       case Nil => None
       case edits =>
-        val content1 = Document_Model.File_Content(text)
+        val content1 = Document_Model.File_Content(node_name, text)
         val pending_edits1 = pending_edits ::: edits
         Some(copy(content = content1, pending_edits = pending_edits1))
     }
@@ -595,7 +604,7 @@
       if (File.is_bib(node_name.node)) {
         bibtex_entries getOrElse {
           val text = JEdit_Lib.buffer_text(buffer)
-          val entries = Bibtex.Entries.parse(text)
+          val entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
           if (entries.errors.nonEmpty) Output.warning(cat_lines(entries.errors))
           bibtex_entries = Some(entries)
           entries