# HG changeset patch
# User wenzelm
# Date 1672078417 -3600
# Node ID de9efab17e4724642798861efeed6168d30bd2c3
# Parent  2735b11a3de8ec02cf9b9f0b38725ec5433eb131# Parent  8ebde8164bbaeca88f14f3145c2743e65c7ba951
merged

diff -r 2735b11a3de8 -r de9efab17e47 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -796,7 +796,7 @@
     def node_required: Boolean
 
     def get_blob: Option[Blob]
-    def bibtex_entries: List[Text.Info[String]]
+    def bibtex_entries: Bibtex.Entries
 
     def node_edits(
       node_header: Node.Header,
diff -r 2735b11a3de8 -r de9efab17e47 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -154,35 +154,61 @@
 
   /* entries */
 
-  def entries(text: String): List[Text.Info[String]] = {
-    val result = new mutable.ListBuffer[Text.Info[String]]
-    var offset = 0
-    for (chunk <- Bibtex.parse(text)) {
-      val end_offset = offset + chunk.source.length
-      if (chunk.name != "" && !chunk.is_command)
-        result += Text.Info(Text.Range(offset, end_offset), chunk.name)
-      offset = end_offset
+  object Entries {
+    val empty: Entries = apply(Nil)
+
+    def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries =
+      new Entries(entries, errors)
+
+    def parse(text: String, file_pos: String = ""): Entries = {
+      val entries = new mutable.ListBuffer[Text.Info[String]]
+      var offset = 0
+      var line = 1
+      var err_line = 0
+
+      try {
+        for (chunk <- Bibtex.parse(text)) {
+          val end_offset = offset + chunk.source.length
+          if (chunk.name != "" && !chunk.is_command) {
+            entries += Text.Info(Text.Range(offset, end_offset), chunk.name)
+          }
+          if (chunk.is_malformed && err_line == 0) { err_line = line }
+          offset = end_offset
+          line += chunk.source.count(_ == '\n')
+        }
+
+        val err_pos =
+          if (err_line == 0 || file_pos.isEmpty) Position.none
+          else Position.Line_File(err_line, file_pos)
+        val errors =
+          if (err_line == 0) Nil
+          else List("Malformed bibtex file" + Position.here(err_pos))
+
+        apply(entries.toList, errors = errors)
+      }
+      catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
     }
-    result.toList
+
+    def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] =
+      for {
+        model <- models.iterator
+        info <- model.bibtex_entries.entries.iterator
+      } yield info.map((_, model))
   }
 
-  def entries_iterator[A, B <: Document.Model](
-    models: Map[A, B]
-  ): Iterator[Text.Info[(String, B)]] = {
-    for {
-      (_, model) <- models.iterator
-      info <- model.bibtex_entries.iterator
-    } yield info.map((_, model))
+  final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
+    def ::: (other: Entries): Entries =
+      new Entries(entries ::: other.entries, errors ::: other.errors)
   }
 
 
   /* completion */
 
-  def completion[A, B <: Document.Model](
+  def completion[A <: Document.Model](
     history: Completion.History,
     rendering: Rendering,
     caret: Text.Offset,
-    models: Map[A, B]
+    models: Iterable[A]
   ): Option[Completion.Result] = {
     for {
       Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
@@ -193,7 +219,7 @@
 
       entries =
         (for {
-          Text.Info(_, (entry, _)) <- entries_iterator(models)
+          Text.Info(_, (entry, _)) <- Entries.iterator(models)
           if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
         } yield entry).toList
       if entries.nonEmpty
@@ -382,7 +408,7 @@
       }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
-    def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
+    def is_malformed: Boolean = tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
     def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
   }
diff -r 2735b11a3de8 -r de9efab17e47 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -439,9 +439,7 @@
               try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
               catch { case ERROR(msg) => List(msg) }
 
-            val bibtex_errors =
-              try { info.bibtex_entries; Nil }
-              catch { case ERROR(msg) => List(msg) }
+            val bibtex_errors = info.bibtex_entries.errors
 
             val base =
               Base(
@@ -639,12 +637,14 @@
 
     def browser_info: Boolean = options.bool("browser_info")
 
-    lazy val bibtex_entries: List[Text.Info[String]] =
+    lazy val bibtex_entries: Bibtex.Entries =
       (for {
         (document_dir, file) <- document_files.iterator
         if File.is_bib(file.file_name)
-        info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
-      } yield info).toList
+      } yield {
+        val path = dir + document_dir + file
+        Bibtex.Entries.parse(File.read(path), file_pos = path.expand.implode)
+      }).foldRight(Bibtex.Entries.empty)(_ ::: _)
 
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 
@@ -923,11 +923,12 @@
     def imports_topological_order: List[String] = imports_graph.topological_order
 
     def bibtex_entries: List[(String, List[String])] =
-      build_topological_order.flatMap(name =>
-        apply(name).bibtex_entries match {
+      build_topological_order.flatMap { name =>
+        apply(name).bibtex_entries.entries match {
           case Nil => None
           case entries => Some(name -> entries.map(_.info))
-        })
+        }
+      }
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 26 19:13:37 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,9 +34,7 @@
 
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
-    lazy val bibtex_entries: List[Text.Info[String]] =
-      try { Bibtex.entries(text) }
-      catch { case ERROR(_) => Nil }
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
 
     def recode_symbols: List[LSP.TextEdit] =
       (for {
@@ -58,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,
@@ -81,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))
@@ -153,8 +149,7 @@
 
   /* bibtex entries */
 
-  def bibtex_entries: List[Text.Info[String]] =
-    model.content.bibtex_entries
+  def bibtex_entries: Bibtex.Entries = model.content.bibtex_entries
 
 
   /* edits */
@@ -166,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) =>
@@ -174,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))
         }
     }
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -78,7 +78,7 @@
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] =
-    Bibtex.entries_iterator(resources.get_models())
+    Bibtex.Entries.iterator(resources.get_models())
 
   def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
     Bibtex.completion(history, rendering, caret, resources.get_models())
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -113,8 +113,8 @@
     else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
   }
 
-  def get_models(): Map[JFile, VSCode_Model] = state.value.models
-  def get_model(file: JFile): Option[VSCode_Model] = get_models().get(file)
+  def get_models(): Iterable[VSCode_Model] = state.value.models.values
+  def get_model(file: JFile): Option[VSCode_Model] = state.value.models.get(file)
   def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name))
 
 
@@ -123,7 +123,7 @@
   def snapshot(model: VSCode_Model): Document.Snapshot =
     model.session.snapshot(
       node_name = model.node_name,
-      pending_edits = Document.Pending_Edits.make(get_models().values))
+      pending_edits = Document.Pending_Edits.make(get_models()))
 
   def get_snapshot(file: JFile): Option[Document.Snapshot] =
     get_model(file).map(snapshot)
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -73,7 +73,8 @@
       if (models.isDefinedAt(node_name)) this
       else {
         val edit = Text.Edit.insert(0, text)
-        val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
+        val content = File_Content(node_name, text)
+        val model = File_Model.init(session, content = content, pending_edits = List(edit))
         copy(models = models + (node_name -> model))
       }
   }
@@ -84,15 +85,16 @@
 
   def document_blobs(): Document.Blobs = state.value.document_blobs
 
-  def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
-  def get_model(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
+  def get_models_map(): Map[Document.Node.Name, Document_Model] = state.value.models
+  def get_models(): Iterable[Document_Model] = get_models_map().values
+  def get_model(name: Document.Node.Name): Option[Document_Model] = get_models_map().get(name)
   def get_model(buffer: JEditBuffer): Option[Buffer_Model] =
     state.value.buffer_models.get(buffer)
 
   def snapshot(model: Document_Model): Document.Snapshot =
     PIDE.session.snapshot(
       node_name = model.node_name,
-      pending_edits = Document.Pending_Edits.make(get_models().values))
+      pending_edits = Document.Pending_Edits.make(get_models()))
 
   def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get_model(name).map(snapshot)
   def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot)
@@ -101,11 +103,11 @@
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
-    Bibtex.entries_iterator(state.value.models)
+    Bibtex.Entries.iterator(get_models())
 
   def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
       : Option[Completion.Result] =
-    Bibtex.completion(history, rendering, caret, state.value.models)
+    Bibtex.completion(history, rendering, caret, get_models())
 
 
   /* overlays */
@@ -131,7 +133,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
@@ -287,12 +289,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: List[Text.Info[String]] =
-      try { Bibtex.entries(text) }
-      catch { case ERROR(_) => Nil }
+    lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node)
   }
 
 
@@ -384,46 +392,43 @@
 }
 
 object File_Model {
-  def empty(session: Session): File_Model =
-    File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
-      false, Document.Node.Perspective_Text.empty, Nil)
-
   def init(session: Session,
-    node_name: Document.Node.Name,
-    text: String,
+    content: Document_Model.File_Content = Document_Model.File_Content.empty,
     node_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
+    val node_name = content.node_name
+
     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 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 =
@@ -441,8 +446,8 @@
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
-  def bibtex_entries: List[Text.Info[String]] =
-    if (File.is_bib(node_name.node)) content.bibtex_entries else Nil
+  def bibtex_entries: Bibtex.Entries =
+    if (File.is_bib(node_name.node)) content.bibtex_entries else Bibtex.Entries.empty
 
 
   /* edits */
@@ -451,7 +456,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))
     }
@@ -502,11 +507,6 @@
 
   /* perspective */
 
-  // owned by GUI thread
-  private var _node_required = false
-  def node_required: Boolean = _node_required
-  def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
-
   def document_view_iterator: Iterator[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer)
@@ -523,88 +523,38 @@
   }
 
 
-  /* blob */
-
-  // owned by GUI thread
-  private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
-
-  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
+  /* mutable buffer state: owned by GUI thread */
 
-  def get_blob: Option[Document.Blob] =
-    GUI_Thread.require {
-      if (is_theory) None
-      else {
-        val (bytes, text, chunk) =
-          _blob match {
-            case Some(x) => x
-            case None =>
-              val bytes = PIDE.resources.make_file_content(buffer)
-              val text = buffer.getText(0, buffer.getLength)
-              val chunk = Symbol.Text_Chunk(text)
-              val x = (bytes, text, chunk)
-              _blob = Some(x)
-              x
-          }
-        val changed = !buffer_edits.is_empty
-        Some(Document.Blob(bytes, text, chunk, changed))
-      }
-    }
-
-
-  /* bibtex entries */
+  private object buffer_state {
+    // perspective and edits
 
-  // owned by GUI thread
-  private var _bibtex_entries: Option[List[Text.Info[String]]] = None
-
-  private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
+    private var last_perspective = Document.Node.Perspective_Text.empty
+    def get_last_perspective: Document.Node.Perspective_Text.T =
+      GUI_Thread.require { last_perspective }
+    def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
+      GUI_Thread.require { last_perspective = perspective }
 
-  def bibtex_entries: List[Text.Info[String]] =
-    GUI_Thread.require {
-      if (File.is_bib(node_name.node)) {
-        _bibtex_entries match {
-          case Some(entries) => entries
-          case None =>
-            val text = JEdit_Lib.buffer_text(buffer)
-            val entries =
-              try { Bibtex.entries(text) }
-              catch { case ERROR(msg) => Output.warning(msg); Nil }
-            _bibtex_entries = Some(entries)
-            entries
-        }
-      }
-      else Nil
-    }
+    private var node_required = false
+    def get_node_required: Boolean = GUI_Thread.require { node_required }
+    def set_node_required(b: Boolean): Unit = GUI_Thread.require { node_required = b }
 
-
-  /* pending buffer edits */
-
-  private object buffer_edits {
-    private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective = Document.Node.Perspective_Text.empty
-
-    def is_empty: Boolean = synchronized { pending.isEmpty }
-    def get_edits: List[Text.Edit] = synchronized { pending.toList }
-    def get_last_perspective: Document.Node.Perspective_Text.T = synchronized { last_perspective }
-    def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
-      synchronized { last_perspective = perspective }
+    private val pending_edits = new mutable.ListBuffer[Text.Edit]
+    def is_stable: Boolean = GUI_Thread.require { pending_edits.isEmpty }
+    def get_pending_edits: List[Text.Edit] = GUI_Thread.require { pending_edits.toList }
 
     def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
-      synchronized {
-        GUI_Thread.require {}
-
-        val edits = get_edits
+      GUI_Thread.require {
+        val edits = get_pending_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
-          pending.clear()
+          pending_edits.clear()
           last_perspective = perspective
           node_edits(node_header(), edits, perspective)
         }
         else Nil
       }
 
-    def edit(edits: List[Text.Edit]): Unit = synchronized {
-      GUI_Thread.require {}
-
+    def edit(edits: List[Text.Edit]): Unit = GUI_Thread.require {
       reset_blob()
       reset_bibtex_entries()
 
@@ -612,16 +562,66 @@
         doc_view.rich_text_area.active_reset()
       }
 
-      pending ++= edits
+      pending_edits ++= edits
       PIDE.editor.invoke()
     }
+
+
+    // blob
+
+    private var blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
+
+    def reset_blob(): Unit = GUI_Thread.require { blob = None }
+
+    def get_blob: Option[Document.Blob] = GUI_Thread.require {
+      if (is_theory) None
+      else {
+        val (bytes, text, chunk) =
+          blob getOrElse {
+            val bytes = PIDE.resources.make_file_content(buffer)
+            val text = buffer.getText(0, buffer.getLength)
+            val chunk = Symbol.Text_Chunk(text)
+            val x = (bytes, text, chunk)
+            blob = Some(x)
+            x
+          }
+        val changed = !is_stable
+        Some(Document.Blob(bytes, text, chunk, changed))
+      }
+    }
+
+
+    // bibtex entries
+
+    private var bibtex_entries: Option[Bibtex.Entries] = None
+
+    def reset_bibtex_entries(): Unit = GUI_Thread.require { bibtex_entries = None }
+
+    def get_bibtex_entries: Bibtex.Entries = GUI_Thread.require {
+      if (File.is_bib(node_name.node)) {
+        bibtex_entries getOrElse {
+          val text = JEdit_Lib.buffer_text(buffer)
+          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
+        }
+      }
+      else Bibtex.Entries.empty
+    }
   }
 
-  def is_stable: Boolean = buffer_edits.is_empty
-  def pending_edits: List[Text.Edit] = buffer_edits.get_edits
+  def is_stable: Boolean = buffer_state.is_stable
+  def pending_edits: List[Text.Edit] = buffer_state.get_pending_edits
+  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
+    buffer_state.flush_edits(doc_blobs, hidden)
 
-  def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
-    buffer_edits.flush_edits(doc_blobs, hidden)
+  def node_required: Boolean = buffer_state.get_node_required
+  def set_node_required(b: Boolean): Unit = buffer_state.set_node_required(b)
+
+  def get_blob: Option[Document.Blob] = buffer_state.get_blob
+
+  def bibtex_entries: Bibtex.Entries = buffer_state.get_bibtex_entries
 
 
   /* buffer listener */
@@ -634,7 +634,7 @@
       num_lines: Int,
       length: Int
     ): Unit = {
-      buffer_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
+      buffer_state.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
     }
 
     override def preContentRemoved(
@@ -644,7 +644,7 @@
       num_lines: Int,
       removed_length: Int
     ): Unit = {
-      buffer_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
+      buffer_state.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
     }
   }
 
@@ -672,16 +672,14 @@
 
   /* init */
 
-  def init(old_model: Option[File_Model]): Buffer_Model = {
-    GUI_Thread.require {}
-
+  def init(old_model: Option[File_Model]): Buffer_Model = GUI_Thread.require {
     old_model match {
       case None =>
-        buffer_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
+        buffer_state.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
         set_node_required(file_model.node_required)
-        buffer_edits.set_last_perspective(file_model.last_perspective)
-        buffer_edits.edit(
+        buffer_state.set_last_perspective(file_model.last_perspective)
+        buffer_state.edit(
           file_model.pending_edits :::
             Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
     }
@@ -695,15 +693,14 @@
 
   /* exit */
 
-  def exit(): File_Model = {
-    GUI_Thread.require {}
-
+  def exit(): File_Model = GUI_Thread.require {
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
-    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
-      node_required = _node_required,
-      last_perspective = buffer_edits.get_last_perspective,
+    File_Model.init(session,
+      content = Document_Model.File_Content(node_name, JEdit_Lib.buffer_text(buffer)),
+      node_required = node_required,
+      last_perspective = buffer_state.get_last_perspective,
       pending_edits = pending_edits)
   }
 }
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -87,7 +87,7 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = {
             Pretty_Tooltip.invoke(() =>
               {
-                val model = File_Model.empty(PIDE.session)
+                val model = File_Model.init(PIDE.session)
                 val rendering = JEdit_Rendering(snapshot, model, options)
                 val info = Text.Info(Text.Range.offside, body)
                 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -59,10 +59,10 @@
   }
 
 
-  /* files */
+  /* plain files */
 
   def is_file(name: String): Boolean =
-    VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
+    name != null && name.nonEmpty && VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
 
   def check_file(name: String): Option[JFile] =
     if (is_file(name)) Some(new JFile(name)) else None
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -32,7 +32,7 @@
   ): (String, JEdit_Rendering) = {
     val command = Command.rich_text(Document_ID.make(), results, formatted_body)
     val snippet = snapshot.snippet(command)
-    val model = File_Model.empty(PIDE.session)
+    val model = File_Model.init(PIDE.session)
     val rendering = apply(snippet, model, PIDE.options.value)
     (command.source, rendering)
   }
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -116,7 +116,7 @@
     def content(): Bytes = Bytes(this.buf, 0, this.count)
   }
 
-  private class File_Content(buffer: Buffer)
+  private class File_Content_Request(buffer: Buffer)
   extends BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath) {
     def _run(): Unit = {}
     def content(): Bytes = {
@@ -126,7 +126,7 @@
     }
   }
 
-  def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+  def make_file_content(buffer: Buffer): Bytes = (new File_Content_Request(buffer)).content()
 
 
   /* theory text edits */
diff -r 2735b11a3de8 -r de9efab17e47 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Mon Dec 26 19:13:37 2022 +0100
@@ -110,7 +110,7 @@
 
   private def delay_load_body(): Unit = {
     val required_files = {
-      val models = Document_Model.get_models()
+      val models = Document_Model.get_models_map()
 
       val thy_files =
         resources.resolve_dependencies(models.values, PIDE.editor.document_required())
@@ -124,7 +124,7 @@
         }
         else Nil
 
-      (thy_files ::: aux_files).filterNot(models.isDefinedAt)
+      (thy_files ::: aux_files).filterNot(models.keySet)
     }
     if (required_files.nonEmpty) {
       try {