more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
prefer global operations for snapshot() and rendering();

--- a/src/Pure/PIDE/document.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -504,6 +504,36 @@
 
   /* snapshot: persistent user-view of document state */
 
+  object Pending_Edits {
+    val empty: Pending_Edits = make(Nil)
+
+    def make(models: Iterable[Model]): Pending_Edits =
+      new Pending_Edits(
+        (for {
+          model <- models.iterator
+          edits = model.pending_edits if edits.nonEmpty
+        } yield model.node_name -> edits).toMap)
+  }
+
+  final class Pending_Edits(pending_edits: Map[Node.Name, List[Text.Edit]]) {
+    def is_stable: Boolean = pending_edits.isEmpty
+
+    def + (entry: (Document.Node.Name, List[Text.Edit])): Pending_Edits = {
+      val (name, es) = entry
+      if (es.isEmpty) this
+      else new Pending_Edits(pending_edits + (name -> (es ::: edits(name))))
+    }
+
+    def edits(name: Document.Node.Name): List[Text.Edit] =
+      pending_edits.getOrElse(name, Nil)
+
+    def reverse_edits(name: Document.Node.Name): List[Text.Edit] =
+      reverse_pending_edits.getOrElse(name, Nil)
+
+    private lazy val reverse_pending_edits =
+      (for ((name, es) <- pending_edits.iterator) yield (name, es.reverse)).toMap
+  }
+
   object Snapshot {
     val init: Snapshot = State.init.snapshot()
   }
@@ -512,13 +542,17 @@
     val state: State,
     val version: Version,
     val node_name: Node.Name,
-    edits: List[Text.Edit],
+    pending_edits: Pending_Edits,
     val snippet_command: Option[Command]
   ) {
     override def toString: String =
       "Snapshot(node = " + node_name.node + ", version = " + version.id +
         (if (is_outdated) ", outdated" else "") + ")"
 
+    def switch(name: Node.Name): Snapshot =
+      if (name == node_name) this
+      else new Snapshot(state, version, name, pending_edits, None)
+
 
     /* nodes */
 
@@ -539,16 +573,14 @@
       }
 
 
-    /* edits */
+    /* pending edits */
 
-    def is_outdated: Boolean = edits.nonEmpty
-
-    private lazy val reverse_edits = edits.reverse
+    def is_outdated: Boolean = !pending_edits.is_stable
 
     def convert(offset: Text.Offset): Text.Offset =
-      edits.foldLeft(offset) { case (i, edit) => edit.convert(i) }
+      pending_edits.edits(node_name).foldLeft(offset) { case (i, edit) => edit.convert(i) }
     def revert(offset: Text.Offset): Text.Offset =
-      reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) }
+      pending_edits.reverse_edits(node_name).foldLeft(offset) { case (i, edit) => edit.revert(i) }
 
     def convert(range: Text.Range): Text.Range = range.map(convert)
     def revert(range: Text.Range): Text.Range = range.map(revert)
@@ -753,7 +785,7 @@
   trait Model {
     def session: Session
     def is_stable: Boolean
-    def snapshot(): Snapshot
+    def pending_edits: List[Text.Edit]
 
     def node_name: Node.Name
     def is_theory: Boolean = node_name.is_theory
@@ -1202,26 +1234,19 @@
 
     def snapshot(
       node_name: Node.Name = Node.Name.empty,
-      pending_edits: List[Text.Edit] = Nil,
+      pending_edits: Pending_Edits = Pending_Edits.empty,
       snippet_command: Option[Command] = None
     ): Snapshot = {
       val stable = recent_stable
       val version = stable.version.get_finished
 
-      val rev_pending_changes =
-        for {
+      val pending_edits1 =
+        (for {
           change <- history.undo_list.takeWhile(_ != stable)
-          (name, edits) <- change.rev_edits
-          if name == node_name
-        } yield edits
+          (name, Node.Edits(es)) <- change.rev_edits
+        } yield (name -> es)).foldLeft(pending_edits)(_ + _)
 
-      val edits =
-        rev_pending_changes.foldLeft(pending_edits) {
-          case (edits, Node.Edits(es)) => es ::: edits
-          case (edits, _) => edits
-        }
-
-      new Snapshot(this, version, node_name, edits, snippet_command)
+      new Snapshot(this, version, node_name, pending_edits1, snippet_command)
     }
 
     def snippet(command: Command): Snapshot =

--- a/src/Pure/PIDE/session.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -688,16 +688,17 @@
     else Document.State.init
   }
 
-  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
-      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
-    get_state().snapshot(name, pending_edits = pending_edits)
+  def snapshot(
+    node_name: Document.Node.Name = Document.Node.Name.empty,
+    pending_edits: Document.Pending_Edits = Document.Pending_Edits.empty
+  ): Document.Snapshot = get_state().snapshot(node_name = node_name, pending_edits = pending_edits)
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.session_base.overall_syntax
 
   def stable_tip_version[A](models: Map[A, Document.Model]): Option[Document.Version] =
-    if (models.valuesIterator.forall(_.is_stable)) get_state().stable_tip_version
+    if (models.forall(p => p._2.pending_edits.isEmpty)) get_state().stable_tip_version
     else None
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot = {

--- a/src/Tools/VSCode/src/dynamic_output.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -21,7 +21,7 @@
         resources.get_caret() match {
           case None => copy(output = Nil)
           case Some(caret) =>
-            val snapshot = caret.model.snapshot()
+            val snapshot = resources.snapshot(caret.model)
             if (do_update && !snapshot.is_outdated) {
               snapshot.current_command(caret.node_name, caret.offset) match {
                 case None => copy(output = Nil)

--- a/src/Tools/VSCode/src/language_server.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -121,9 +121,8 @@
 
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
-      model <- resources.get_model(new JFile(node_pos.name))
-      rendering = model.rendering()
-      offset <- model.content.doc.offset(node_pos.pos)
+      rendering <- resources.get_rendering(new JFile(node_pos.name))
+      offset <- rendering.model.content.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
   private val dynamic_output = Dynamic_Output(server)
@@ -366,7 +365,7 @@
     for {
       spell_checker <- resources.spell_checker.get
       caret <- resources.get_caret()
-      rendering = caret.model.rendering()
+      rendering = resources.rendering(caret.model)
       range = rendering.before_caret_range(caret.offset)
       Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
     } {
@@ -493,11 +492,11 @@
     override def current_node(context: Unit): Option[Document.Node.Name] =
       resources.get_caret().map(_.model.node_name)
     override def current_node_snapshot(context: Unit): Option[Document.Snapshot] =
-      resources.get_caret().map(_.model.snapshot())
+      resources.get_caret().map(caret => resources.snapshot(caret.model))
 
     override def node_snapshot(name: Document.Node.Name): Document.Snapshot = {
-      resources.get_model(name) match {
-        case Some(model) => model.snapshot()
+      resources.get_snapshot(name) match {
+        case Some(snapshot) => snapshot
         case None => session.snapshot(name)
       }
     }

--- a/src/Tools/VSCode/src/preview_panel.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -25,7 +25,7 @@
           case (m, (file, column)) =>
             resources.get_model(file) match {
               case Some(model) =>
-                val snapshot = model.snapshot()
+                val snapshot = resources.snapshot(model)
                 if (snapshot.is_outdated) m
                 else {
                   val context =

--- a/src/Tools/VSCode/src/vscode_model.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -78,6 +78,7 @@
 ) extends Document.Model {
   model =>
 
+
   /* content */
 
   def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -106,7 +107,7 @@
     caret: Option[Line.Position]
   ): (Boolean, Document.Node.Perspective_Text.T) = {
     if (is_theory) {
-      val snapshot = model.snapshot()
+      val snapshot = resources.snapshot(model)
 
       val required = node_required || editor.document_node_required(node_name)
 
@@ -231,12 +232,6 @@
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
   def is_stable: Boolean = pending_edits.isEmpty
-  def snapshot(): Document.Snapshot =
-    session.snapshot(node_name, pending_edits = pending_edits)
-
-  def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
-    new VSCode_Rendering(snapshot, model)
-  def rendering(): VSCode_Rendering = rendering(snapshot())
 
 
   /* syntax */

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -78,10 +78,10 @@
   /* 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)
+    Bibtex.completion(history, rendering, caret, resources.get_models())
 
 
   /* completion */

--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -113,11 +113,39 @@
     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(): Map[JFile, VSCode_Model] = state.value.models
+  def get_model(file: JFile): Option[VSCode_Model] = get_models().get(file)
   def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name))
 
 
+  /* snapshot */
+
+  def snapshot(model: VSCode_Model): Document.Snapshot =
+    model.session.snapshot(
+      node_name = model.node_name,
+      pending_edits = Document.Pending_Edits.make(get_models().values))
+
+  def get_snapshot(file: JFile): Option[Document.Snapshot] =
+    get_model(file).map(snapshot)
+
+  def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] =
+    get_model(name).map(snapshot)
+
+
+  /* rendering */
+
+  def rendering(snapshot: Document.Snapshot, model: VSCode_Model): VSCode_Rendering =
+    new VSCode_Rendering(snapshot, model)
+
+  def rendering(model: VSCode_Model): VSCode_Rendering = rendering(snapshot(model), model)
+
+  def get_rendering(file: JFile): Option[VSCode_Rendering] =
+    get_model(file).map(rendering)
+
+  def get_rendering(name: Document.Node.Name): Option[VSCode_Rendering] =
+    get_model(name).map(rendering)
+
+
   /* file content */
 
   def read_file_content(name: Document.Node.Name): Option[String] = {
@@ -275,7 +303,7 @@
         (for {
           file <- st.pending_output.iterator
           model <- st.models.get(file)
-        } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
+        } yield (file, model, rendering(model))).toList.partition(_._3.snapshot.is_outdated)
 
       val changed_iterator =
         for {

--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -176,7 +176,7 @@
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = {
     val opt_snapshot =
       Document_Model.get(buffer) match {
-        case Some(model) if model.is_theory => Some(model.snapshot())
+        case Some(model) if model.is_theory => Some(Document_Model.snapshot(model))
         case _ => None
       }
     opt_snapshot match {

--- a/src/Tools/jEdit/src/active.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/active.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -28,7 +28,7 @@
     Document_View.get(view.getTextArea) match {
       case Some(doc_view) =>
         doc_view.rich_text_area.robust_body(()) {
-          val snapshot = doc_view.model.snapshot()
+          val snapshot = Document_Model.snapshot(doc_view.model)
           if (!snapshot.is_outdated) {
             handlers.find(_.handle(view, text, elem, doc_view, snapshot))
           }

--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -281,7 +281,7 @@
 
       if (buffer.isEditable) {
         val caret = text_area.getCaretPosition
-        val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
+        val opt_rendering = Document_View.get_rendering(text_area)
         val result0 = syntax_completion(history, explicit, opt_rendering)
         val (no_completion, semantic_completion) = {
           opt_rendering match {

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -33,7 +33,7 @@
 
     Document_View.get(text_area) match {
       case Some(doc_view) =>
-        val rendering = doc_view.get_rendering()
+        val rendering = Document_View.rendering(doc_view)
         val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
         rendering.breakpoint(range)
       case None => None

--- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -82,11 +82,19 @@
 
   def reset(): Unit = state.change(_ => State())
 
+  def document_blobs(): Document.Blobs = state.value.document_blobs
+
   def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
   def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
-  def document_blobs(): Document.Blobs = state.value.document_blobs
+  def snapshot(model: Document_Model): Document.Snapshot =
+    PIDE.session.snapshot(
+      node_name = model.node_name,
+      pending_edits = Document.Pending_Edits.make(get_models().values))
+
+  def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get(name).map(snapshot)
+  def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get(buffer).map(snapshot)
 
 
   /* bibtex */
@@ -328,6 +336,9 @@
 }
 
 sealed abstract class Document_Model extends Document.Model {
+  model =>
+
+
   /* perspective */
 
   def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
@@ -339,7 +350,7 @@
     GUI_Thread.require {}
 
     if (JEdit_Options.continuous_checking() && is_theory) {
-      val snapshot = this.snapshot()
+      val snapshot = Document_Model.snapshot(model)
 
       val required = node_required || PIDE.editor.document_node_required(node_name)
 
@@ -362,7 +373,7 @@
   /* snapshot */
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot = {
-    val snapshot = this.snapshot()
+    val snapshot = Document_Model.snapshot(model)
     if (snapshot.is_outdated) {
       PIDE.session.output_delay.sleep()
       await_stable_snapshot()
@@ -465,12 +476,7 @@
       Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty))
     }
 
-
-  /* snapshot */
-
   def is_stable: Boolean = pending_edits.isEmpty
-  def snapshot(): Document.Snapshot =
-    session.snapshot(node_name, pending_edits = pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
@@ -611,10 +617,7 @@
   }
 
   def is_stable: Boolean = buffer_edits.is_empty
-  def pending_edits(): List[Text.Edit] = buffer_edits.get_edits
-
-  def snapshot(): Document.Snapshot =
-    session.snapshot(node_name, pending_edits = pending_edits())
+  def pending_edits: List[Text.Edit] = buffer_edits.get_edits
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     buffer_edits.flush_edits(doc_blobs, hidden)
@@ -700,6 +703,6 @@
     File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
       node_required = _node_required,
       last_perspective = buffer_edits.get_last_perspective,
-      pending_edits = pending_edits())
+      pending_edits = pending_edits)
   }
 }

--- a/src/Tools/jEdit/src/document_view.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -49,17 +49,25 @@
     doc_view.activate()
     doc_view
   }
+
+  def rendering(doc_view: Document_View): JEdit_Rendering = {
+    val model = doc_view.model
+    val snapshot = Document_Model.snapshot(model)
+    val options = PIDE.options.value
+    JEdit_Rendering(snapshot, model, options)
+  }
+
+  def get_rendering(text_area: TextArea): Option[JEdit_Rendering] = get(text_area).map(rendering)
 }
 
+class Document_View(val model: Buffer_Model, val text_area: JEditTextArea) {
+  doc_view =>
 
-class Document_View(val model: Buffer_Model, val text_area: JEditTextArea) {
   private val session = model.session
 
-  def get_rendering(): JEdit_Rendering =
-    JEdit_Rendering(model.snapshot(), model, PIDE.options.value)
-
-  val rich_text_area =
-    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
+  val rich_text_area: Rich_Text_Area =
+    new Rich_Text_Area(text_area.getView, text_area,
+      () => Document_View.rendering(doc_view), () => (), () => None,
       () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
 
 
@@ -138,7 +146,7 @@
 
         val buffer = model.buffer
         JEdit_Lib.buffer_lock(buffer) {
-          val rendering = get_rendering()
+          val rendering = Document_View.rendering(doc_view)
 
           for (i <- physical_lines.indices) {
             if (physical_lines(i) != -1) {
@@ -199,7 +207,7 @@
   /* text status overview left of scrollbar */
 
   private val text_overview: Option[Text_Overview] =
-    if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(this)) else None
+    if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(doc_view)) else None
 
 
   /* main */
@@ -214,7 +222,7 @@
         GUI_Thread.later {
           JEdit_Lib.buffer_lock(buffer) {
             if (model.buffer == text_area.getBuffer) {
-              val snapshot = model.snapshot()
+              val snapshot = Document_Model.snapshot(model)
 
               if (changed.assignment ||
                   (changed.nodes.contains(model.node_name) &&

--- a/src/Tools/jEdit/src/isabelle.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -365,16 +365,14 @@
   def goto_entity(view: View): Unit = {
     val text_area = view.getTextArea
     for {
-      doc_view <- Document_View.get(text_area)
-      rendering = doc_view.get_rendering()
+      rendering <- Document_View.get_rendering(text_area)
       caret_range = JEdit_Lib.caret_range(text_area)
       link <- rendering.hyperlink_entity(caret_range)
     } link.info.follow(view)
   }
 
   def select_entity(text_area: JEditTextArea): Unit = {
-    for (doc_view <- Document_View.get(text_area)) {
-      val rendering = doc_view.get_rendering()
+    for (rendering <- Document_View.get_rendering(text_area)) {
       val caret_range = JEdit_Lib.caret_range(text_area)
       val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
       val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
@@ -431,8 +429,7 @@
   def antiquoted_cartouche(text_area: TextArea): Unit = {
     val buffer = text_area.getBuffer
     for {
-      doc_view <- Document_View.get(text_area)
-      rendering = doc_view.get_rendering()
+      rendering <- Document_View.get_rendering(text_area)
       caret_range = JEdit_Lib.caret_range(text_area)
       antiq_range <- rendering.antiquoted(caret_range)
       antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
@@ -461,8 +458,7 @@
   def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean): Unit = {
     for {
       spell_checker <- PIDE.plugin.spell_checker.get
-      doc_view <- Document_View.get(text_area)
-      rendering = doc_view.get_rendering()
+      rendering <- Document_View.get_rendering(text_area)
       range = JEdit_Lib.caret_range(text_area)
       Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
     } {
@@ -527,8 +523,7 @@
     val painter = text_area.getPainter
     val caret_range = JEdit_Lib.caret_range(text_area)
     for {
-      doc_view <- Document_View.get(text_area)
-      rendering = doc_view.get_rendering()
+      rendering <- Document_View.get_rendering(text_area)
       tip <- rendering.tooltip(caret_range, control)
       loc0 <- Option(text_area.offsetToXY(caret_range.start))
     } {
@@ -551,8 +546,7 @@
     GUI_Thread.require {}
 
     val text_area = view.getTextArea
-    for (doc_view <- Document_View.get(text_area)) {
-      val rendering = doc_view.get_rendering()
+    for (rendering <- Document_View.get_rendering(text_area)) {
       val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
       get(errs) match {
         case Some(err) =>

--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -70,15 +70,10 @@
     GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
 
   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
-    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
+    GUI_Thread.require { Document_Model.get_snapshot(view.getBuffer) }
 
-  override def node_snapshot(name: Document.Node.Name): Document.Snapshot = {
-    GUI_Thread.require {}
-    Document_Model.get(name) match {
-      case Some(model) => model.snapshot()
-      case None => session.snapshot(name)
-    }
-  }
+  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
+    GUI_Thread.require { Document_Model.get_snapshot(name) getOrElse session.snapshot(name) }
 
   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = {
     GUI_Thread.require {}

--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -38,8 +38,7 @@
     val result =
       for {
         spell_checker <- PIDE.plugin.spell_checker.get
-        doc_view <- Document_View.get(text_area)
-        rendering = doc_view.get_rendering()
+        rendering <- Document_View.get_rendering(text_area)
         range = JEdit_Lib.point_range(text_area.getBuffer, offset)
         Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
       } yield (spell_checker, word)

--- a/src/Tools/jEdit/src/main_plugin.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -27,12 +27,12 @@
 
   def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now {
     val buffer = JEdit_Lib.jedit_view(view).getBuffer
-    Document_Model.get(buffer).map(_.snapshot())
+    Document_Model.get_snapshot(buffer)
   }
 
   def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now {
     val text_area = JEdit_Lib.jedit_view(view).getTextArea
-    Document_View.get(text_area).map(_.get_rendering())
+    Document_View.get_rendering(text_area)
   }
 
   def snapshot(view: View = null): Document.Snapshot =

--- a/src/Tools/jEdit/src/text_overview.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -82,7 +82,7 @@
 
     doc_view.rich_text_area.robust_body(()) {
       JEdit_Lib.buffer_lock(buffer) {
-        val rendering = doc_view.get_rendering()
+        val rendering = Document_View.rendering(doc_view)
         val overview = get_overview()
 
         if (rendering.snapshot.is_outdated || overview != current_overview) {
@@ -118,7 +118,7 @@
       if (!doc_view.rich_text_area.check_robust_body) invoke()
       else {
         JEdit_Lib.buffer_lock(buffer) {
-          val rendering = doc_view.get_rendering()
+          val rendering = Document_View.rendering(doc_view)
           val overview = get_overview()
 
           if (rendering.snapshot.is_outdated || is_running()) invoke()

--- a/src/Tools/jEdit/src/text_structure.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -92,8 +92,8 @@
                 GUI_Thread.now {
                   (for {
                     text_area <- JEdit_Lib.jedit_text_areas(buffer)
-                    doc_view <- Document_View.get(text_area)
-                  } yield doc_view.get_rendering()).nextOption()
+                    rendering <- Document_View.get_rendering(text_area)
+                  } yield rendering).nextOption()
                 }
               else None
             val limit = PIDE.options.value.int("jedit_indent_script_limit")