# HG changeset patch # User wenzelm # Date 1671831707 -3600 # Node ID c654103e9c9d2c7b2106a9843f516f1d8a008737 # Parent 10f155d5f34b0a0d1329e227f983c51e83c19ca3 more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch; prefer global operations for snapshot() and rendering(); diff -r 10f155d5f34b -r c654103e9c9d src/Pure/PIDE/document.scala --- 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 = diff -r 10f155d5f34b -r c654103e9c9d src/Pure/PIDE/session.scala --- 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 = { diff -r 10f155d5f34b -r c654103e9c9d src/Tools/VSCode/src/dynamic_output.scala --- 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) diff -r 10f155d5f34b -r c654103e9c9d src/Tools/VSCode/src/language_server.scala --- 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) } } diff -r 10f155d5f34b -r c654103e9c9d src/Tools/VSCode/src/preview_panel.scala --- 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 = diff -r 10f155d5f34b -r c654103e9c9d src/Tools/VSCode/src/vscode_model.scala --- 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 */ diff -r 10f155d5f34b -r c654103e9c9d src/Tools/VSCode/src/vscode_rendering.scala --- 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 */ diff -r 10f155d5f34b -r c654103e9c9d src/Tools/VSCode/src/vscode_resources.scala --- 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 { diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- 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 { diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/active.scala --- 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)) } diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/completion_popup.scala --- 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 { diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/debugger_dockable.scala --- 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 diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/document_model.scala --- 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) } } diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/document_view.scala --- 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) && diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/isabelle.scala --- 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) => diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/jedit_editor.scala --- 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 {} diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/jedit_spell_checker.scala --- 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) diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/main_plugin.scala --- 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 = diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/text_overview.scala --- 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() diff -r 10f155d5f34b -r c654103e9c9d src/Tools/jEdit/src/text_structure.scala --- 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")