# HG changeset patch # User desharna # Date 1672059846 -3600 # Node ID 2735b11a3de8ec02cf9b9f0b38725ec5433eb131 # Parent 602ddfb744b1a5f4bb889f97828e0bf759eb30d4# Parent b61ad889dffa6b8920e18337862031d7e6b2cf94 merged diff -r b61ad889dffa -r 2735b11a3de8 src/Doc/System/Scala.thy --- a/src/Doc/System/Scala.thy Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Doc/System/Scala.thy Mon Dec 26 14:04:06 2022 +0100 @@ -152,7 +152,7 @@ \<^medskip> The syntax of \<^path>\etc/build.props\ follows a regular Java properties - file\<^footnote>\\<^url>\https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\\, + file\<^footnote>\\<^url>\https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\\, but the encoding is \<^verbatim>\UTF-8\, instead of historic \<^verbatim>\ISO 8859-1\ from the API documentation. diff -r b61ad889dffa -r 2735b11a3de8 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Mon Dec 26 13:54:07 2022 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Mon Dec 26 14:04:06 2022 +0100 @@ -617,6 +617,74 @@ end + +context + fixes f::"'a \ 'b::{conditionally_complete_linorder,ordered_ab_group_add}" +begin + +lemma bdd_above_uminus_image: "bdd_above ((\x. - f x) ` A) \ bdd_below (f ` A)" + by (metis bdd_above_uminus image_image) + +lemma bdd_below_uminus_image: "bdd_below ((\x. - f x) ` A) \ bdd_above (f ` A)" + by (metis bdd_below_uminus image_image) + +lemma uminus_cSUP: + assumes "bdd_above (f ` A)" "A \ {}" + shows "- (SUP x\A. f x) = (INF x\A. - f x)" +proof (rule antisym) + show "(INF x\A. - f x) \ - Sup (f ` A)" + by (metis cINF_lower cSUP_least bdd_below_uminus_image assms le_minus_iff) + have *: "\x. x \A \ f x \ Sup (f ` A)" + by (simp add: assms cSup_upper) + then show "- Sup (f ` A) \ (INF x\A. - f x)" + by (simp add: assms cINF_greatest) +qed + +end + +context + fixes f::"'a \ 'b::{conditionally_complete_linorder,ordered_ab_group_add}" +begin + +lemma uminus_cINF: + assumes "bdd_below (f ` A)" "A \ {}" + shows "- (INF x\A. f x) = (SUP x\A. - f x)" + by (metis (mono_tags, lifting) INF_cong uminus_cSUP assms bdd_above_uminus_image minus_equation_iff) + +lemma Sup_add_eq: + assumes "bdd_above (f ` A)" "A \ {}" + shows "(SUP x\A. a + f x) = a + (SUP x\A. f x)" (is "?L=?R") +proof (rule antisym) + have bdd: "bdd_above ((\x. a + f x) ` A)" + by (metis assms bdd_above_image_mono image_image mono_add) + with assms show "?L \ ?R" + by (simp add: assms cSup_le_iff cSUP_upper) + have "\x. x \ A \ f x \ (SUP x\A. a + f x) - a" + by (simp add: bdd cSup_upper le_diff_eq) + with \A \ {}\ have "\ (f ` A) \ (\x\A. a + f x) - a" + by (simp add: cSUP_least) + then show "?R \ ?L" + by (metis add.commute le_diff_eq) +qed + +lemma Inf_add_eq: \\you don't get a shorter proof by duality\ + assumes "bdd_below (f ` A)" "A \ {}" + shows "(INF x\A. a + f x) = a + (INF x\A. f x)" (is "?L=?R") +proof (rule antisym) + show "?R \ ?L" + using assms mono_add mono_cINF by blast + have bdd: "bdd_below ((\x. a + f x) ` A)" + by (metis add_left_mono assms(1) bdd_below.E bdd_below.I2 imageI) + with assms have "\x. x \ A \ f x \ (INF x\A. a + f x) - a" + by (simp add: cInf_lower diff_le_eq) + with \A \ {}\ have "(\x\A. a + f x) - a \ \ (f ` A)" + by (simp add: cINF_greatest) + with assms show "?L \ ?R" + by (metis add.commute diff_le_eq) +qed + +end + instantiation nat :: conditionally_complete_linorder begin diff -r b61ad889dffa -r 2735b11a3de8 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Pure/PIDE/document.scala Mon Dec 26 14:04:06 2022 +0100 @@ -319,9 +319,10 @@ def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this - else + else { new Node(get_blob, header, syntax, text_perspective, perspective, Node.Commands(new_commands)) + } def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = _commands.iterator(i) @@ -503,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() } @@ -511,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 */ @@ -538,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) @@ -752,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 @@ -993,9 +1026,12 @@ val edited_nodes = (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList - def upd(exec_id: Document_ID.Exec, st: Command.State) - : Option[(Document_ID.Exec, Command.State)] = + def upd( + exec_id: Document_ID.Exec, + st: Command.State + ): Option[(Document_ID.Exec, Command.State)] = { if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) + } val (changed_commands, new_execs) = update.foldLeft((List.empty[Command], execs)) { @@ -1071,13 +1107,15 @@ blobs1 += digest } - if (!commands1.isDefinedAt(command.id)) + if (!commands1.isDefinedAt(command.id)) { commands.get(command.id).foreach(st => commands1 += (command.id -> st)) + } - for (exec_id <- command_execs.getOrElse(command.id, Nil)) { - if (!execs1.isDefinedAt(exec_id)) - execs.get(exec_id).foreach(st => execs1 += (exec_id -> st)) - } + for { + exec_id <- command_execs.getOrElse(command.id, Nil) + if !execs1.isDefinedAt(exec_id) + st <- execs.get(exec_id) + } execs1 += (exec_id -> st) } copy( @@ -1196,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 b61ad889dffa -r 2735b11a3de8 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Pure/PIDE/resources.scala Mon Dec 26 14:04:06 2022 +0100 @@ -458,18 +458,19 @@ /* resolve implicit theory dependencies */ def resolve_dependencies[A]( - models: Map[A, Document.Model], - theories: List[(Document.Node.Name, Position.T)] + models: Iterable[Document.Model], + theories: List[Document.Node.Name] ): List[Document.Node.Name] = { val model_theories = - (for (model <- models.valuesIterator if model.is_theory) + (for (model <- models.iterator if model.is_theory) yield (model.node_name, Position.none)).toList - val thy_files1 = dependencies(model_theories ::: theories).theories + val thy_files1 = + dependencies(model_theories ::: theories.map((_, Position.none))).theories val thy_files2 = (for { - model <- models.valuesIterator if !model.is_theory + model <- models.iterator if !model.is_theory thy_name <- make_theory_name(model.node_name) } yield thy_name).toList diff -r b61ad889dffa -r 2735b11a3de8 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Pure/PIDE/session.scala Mon Dec 26 14:04:06 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) + 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 + def stable_tip_version[A](models: Iterable[Document.Model]): Option[Document.Version] = + if (models.forall(model => model.pending_edits.isEmpty)) get_state().stable_tip_version else None @tailrec final def await_stable_snapshot(): Document.Snapshot = { diff -r b61ad889dffa -r 2735b11a3de8 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Pure/Thy/document_build.scala Mon Dec 26 14:04:06 2022 +0100 @@ -132,6 +132,17 @@ List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty"). map(name => texinputs + Path.basic(name)) + def running_script(title: String): String = "echo 'Running " + quote(title) + " ...'; " + def is_running_script(msg: String): Boolean = + msg.startsWith("Running \"") && msg.endsWith("\" ...") + + sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) { + def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body) + def file_pos: String = name.path.implode_symbolic + def write(latex_output: Latex.Output, dir: Path): Unit = + content.output(latex_output(_, file_pos = file_pos)).write(dir) + } + def context( session_context: Export.Session_Context, document_session: Option[Sessions.Base] = None, @@ -185,19 +196,15 @@ def session_document_theories: List[Document.Node.Name] = base.proper_session_theories def all_document_theories: List[Document.Node.Name] = base.all_document_theories - lazy val document_latex: List[(File.Content_XML, String)] = - for (name <- all_document_theories) - yield { - val path = Path.basic(tex_name(name)) - val content = - if (document_selection(name)) { - val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) - YXML.parse_body(entry.text) - } - else Nil - val file_pos = name.path.implode_symbolic - (File.content(path, content), file_pos) - } + lazy val isabelle_logo: Option[File.Content] = { + document_logo.map(logo_name => + Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path => + Logo.create_logo(logo_name, output_file = tmp_path, quiet = true) + val path = Path.basic("isabelle_logo.pdf") + val content = Bytes.read(tmp_path) + File.content(path, content) + }) + } lazy val session_graph: File.Content = { val path = Browser_Info.session_graph_path @@ -213,15 +220,17 @@ File.content(path, content) } - lazy val isabelle_logo: Option[File.Content] = { - document_logo.map(logo_name => - Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path => - Logo.create_logo(logo_name, output_file = tmp_path, quiet = true) - val path = Path.basic("isabelle_logo.pdf") - val content = Bytes.read(tmp_path) - File.content(path, content) - }) - } + lazy val document_latex: List[Document_Latex] = + for (name <- all_document_theories) + yield { + val body = + if (document_selection(name)) { + val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true) + YXML.parse_body(entry.text) + } + else Nil + Document_Latex(name, body) + } /* build document */ @@ -263,11 +272,7 @@ } session_tex.write(doc_dir) - - for ((content, file_pos) <- document_latex) { - content.output(latex_output(_, file_pos = file_pos)) - .write(doc_dir) - } + document_latex.foreach(_.write(latex_output, doc_dir)) val root_name1 = "root_" + doc.name val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root" @@ -280,7 +285,6 @@ /* derived material: without SHA1 digest */ isabelle_logo.foreach(_.write(doc_dir)) - session_graph.write(doc_dir) Directory(doc_dir, doc, root_name, sources) @@ -304,12 +308,16 @@ def root_name_script(ext: String = ""): String = Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext) - def conditional_script(ext: String, exe: String, after: String = ""): String = + def conditional_script( + ext: String, exe: String, title: String = "", after: String = "" + ): String = { "if [ -f " + root_name_script(ext) + " ]\n" + "then\n" + - " " + exe + " " + root_name_script() + "\n" + + " " + (if (title.nonEmpty) running_script(title) else "") + + exe + " " + root_name_script() + "\n" + (if (after.isEmpty) "" else " " + after) + "fi\n" + } def log_errors(): List[String] = Latex.latex_errors(doc_dir, root_name) ::: @@ -350,18 +358,19 @@ context.prepare_directory(dir, doc, new Latex.Output(context.options)) def use_pdflatex: Boolean = false + def running_latex: String = running_script(if (use_pdflatex) "pdflatex" else "lualatex") def latex_script(context: Context, directory: Directory): String = - (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") + + running_latex + (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") + " " + directory.root_name_script() + "\n" def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = { val ext = if (context.document_bibliography) "aux" else "bib" - directory.conditional_script(ext, "$ISABELLE_BIBTEX", + directory.conditional_script(ext, "$ISABELLE_BIBTEX", title = "bibtex", after = if (latex) latex_script(context, directory) else "") } def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String = - directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", + directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", title = "makeindex", after = if (latex) latex_script(context, directory) else "") def use_build_script: Boolean = false diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/VSCode/src/dynamic_output.scala --- a/src/Tools/VSCode/src/dynamic_output.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/VSCode/src/dynamic_output.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/VSCode/src/preview_panel.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/vscode_model.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_model.scala Mon Dec 26 14:04:06 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,11 +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) - - def rendering(snapshot: Document.Snapshot): VSCode_Rendering = - new VSCode_Rendering(snapshot, model) - def rendering(): VSCode_Rendering = rendering(snapshot()) /* syntax */ diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Dec 26 14:04:06 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] = { @@ -207,11 +235,10 @@ file_watcher: File_Watcher ): (Boolean, Boolean) = { state.change_result { st => - val stable_tip_version = session.stable_tip_version(st.models) + val stable_tip_version = session.stable_tip_version(st.models.values) val thy_files = - resources.resolve_dependencies(st.models, - editor.document_required().map((_, Position.none))) + resources.resolve_dependencies(st.models.values, editor.document_required()) val aux_files = stable_tip_version.toList.flatMap(undefined_blobs) @@ -275,7 +302,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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Mon Dec 26 14:04:06 2022 +0100 @@ -175,8 +175,8 @@ class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") { 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()) + Document_Model.get_model(buffer) match { + case Some(model) if model.is_theory => Some(Document_Model.snapshot(model)) case _ => None } opt_snapshot match { diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/active.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Mon Dec 26 14:04:06 2022 +0100 @@ -106,7 +106,7 @@ } private val scroll_log_area = new ScrollPane(log_area) - def log_progress(): Document_Editor.Log_Progress = + def log_progress(only_running: Boolean = false): Document_Editor.Log_Progress = new Document_Editor.Log_Progress(PIDE.session) { override def show(text: String): Unit = if (text != log_area.text) { @@ -114,6 +114,8 @@ val vertical = scroll_log_area.peer.getVerticalScrollBar vertical.setValue(vertical.getMaximum) } + override def echo(msg: String): Unit = + if (!only_running || Document_Build.is_running_script(msg)) super.echo(msg) } @@ -131,11 +133,13 @@ private def finish_process(output: List[XML.Tree]): Unit = current_state.change(_.finish(output)) - private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = { + private def run_process(only_running: Boolean = false)( + body: Document_Editor.Log_Progress => Unit + ): Boolean = { val started = current_state.change_result { st => if (st.process.is_finished) { - val progress = log_progress() + val progress = log_progress(only_running = only_running) val process = Future.thread[Unit](name = "Document_Dockable.process") { await_process() @@ -151,7 +155,7 @@ private def load_document(session: String): Boolean = { val options = PIDE.options.value - run_process { _ => + run_process() { _ => try { val session_background = Document_Build.session_background( @@ -212,7 +216,7 @@ private def build_document(): Unit = { PIDE.editor.document_session() match { case Some(session_background) if session_background.info.documents.nonEmpty => - run_process { progress => + run_process(only_running = true) { progress => show_page(log_page) val result = Exn.capture { document_build(session_background, progress) } val msgs = diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Mon Dec 26 14:04:06 2022 +0100 @@ -82,11 +82,20 @@ 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 get_model(name: Document.Node.Name): Option[Document_Model] = get_models().get(name) + def get_model(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_model(name).map(snapshot) + def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot) /* bibtex */ @@ -218,7 +227,7 @@ toggle: Boolean = false, set: Boolean = false ): Unit = - Document_Model.get(view.getBuffer).foreach(model => + Document_Model.get_model(view.getBuffer).foreach(model => node_required(model.node_name, toggle = toggle, set = set)) @@ -290,7 +299,7 @@ /* HTTP preview */ def open_preview(view: View, plain_text: Boolean): Unit = { - Document_Model.get(view.getBuffer) match { + Document_Model.get_model(view.getBuffer) match { case Some(model) => val url = Preview_Service.server_url(plain_text, model.node_name) PIDE.editor.hyperlink_url(url).follow(view) @@ -311,7 +320,7 @@ for { query <- request.decode_query name = Library.perhaps_unprefix(plain_text_prefix, query) - model <- get(PIDE.resources.node_name(name)) + model <- get_model(PIDE.resources.node_name(name)) } yield { val snapshot = model.await_stable_snapshot() @@ -328,6 +337,9 @@ } sealed abstract class Document_Model extends Document.Model { + model => + + /* perspective */ def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil @@ -339,7 +351,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 +374,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,11 +477,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) } case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) @@ -537,7 +545,7 @@ _blob = Some(x) x } - val changed = pending_edits.nonEmpty + val changed = !buffer_edits.is_empty Some(Document.Blob(bytes, text, chunk, changed)) } } @@ -568,13 +576,13 @@ } - /* pending edits */ + /* pending buffer edits */ - private object pending_edits { + private object buffer_edits { private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective = Document.Node.Perspective_Text.empty - def nonEmpty: Boolean = synchronized { pending.nonEmpty } + 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 = @@ -600,19 +608,20 @@ reset_blob() reset_bibtex_entries() - for (doc_view <- document_view_iterator) + for (doc_view <- document_view_iterator) { doc_view.rich_text_area.active_reset() + } pending ++= edits PIDE.editor.invoke() } } - def is_stable: Boolean = !pending_edits.nonEmpty - def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits) + def is_stable: Boolean = buffer_edits.is_empty + def pending_edits: List[Text.Edit] = buffer_edits.get_edits def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = - pending_edits.flush_edits(doc_blobs, hidden) + buffer_edits.flush_edits(doc_blobs, hidden) /* buffer listener */ @@ -625,7 +634,7 @@ num_lines: Int, length: Int ): Unit = { - pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) + buffer_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) } override def preContentRemoved( @@ -635,7 +644,7 @@ num_lines: Int, removed_length: Int ): Unit = { - pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) + buffer_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) } } @@ -644,9 +653,10 @@ def syntax_changed(): Unit = { JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0) - for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) + for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) { Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). invoke(text_area) + } buffer.invalidateCachedFoldLevels() } @@ -667,11 +677,11 @@ old_model match { case None => - pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) + buffer_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) case Some(file_model) => set_node_required(file_model.node_required) - pending_edits.set_last_perspective(file_model.last_perspective) - pending_edits.edit( + buffer_edits.set_last_perspective(file_model.last_perspective) + buffer_edits.edit( file_model.pending_edits ::: Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) } @@ -693,7 +703,7 @@ File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required = _node_required, - last_perspective = pending_edits.get_last_perspective, - pending_edits = pending_edits.get_edits) + last_perspective = buffer_edits.get_last_perspective, + pending_edits = pending_edits) } } diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Dec 26 14:04:06 2022 +0100 @@ -60,7 +60,7 @@ def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] = if (buffer == null) None else - (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match { + (JEdit_Lib.buffer_mode(buffer), Document_Model.get_model(buffer)) match { case ("isabelle", Some(model)) => Some(PIDE.session.recent_syntax(model.node_name)) case (mode, _) => mode_syntax(mode) @@ -328,7 +328,7 @@ ): Unit = { val buffer = text_area.getBuffer if (!snapshot.is_outdated && text != "") { - (snapshot.find_command(id), Document_Model.get(buffer)) match { + (snapshot.find_command(id), Document_Model.get_model(buffer)) match { case (Some((node, command)), Some(model)) if command.node_name == model.node_name => node.command_start(command) match { case Some(start) => @@ -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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Dec 26 14:04:06 2022 +0100 @@ -67,18 +67,13 @@ /* current situation */ override def current_node(view: View): Option[Document.Node.Name] = - GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } + GUI_Thread.require { Document_Model.get_model(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 {} @@ -90,7 +85,7 @@ case Some(doc_view) if doc_view.model.is_theory => snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition) case _ => - Document_Model.get(buffer) match { + Document_Model.get_model(buffer) match { case Some(model) if !model.is_theory => snapshot.version.nodes.commands_loading(model.node_name).headOption case _ => None diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Dec 26 14:04:06 2022 +0100 @@ -86,7 +86,7 @@ } def get_file_content(node_name: Document.Node.Name): Option[String] = - Document_Model.get(node_name) match { + Document_Model.get_model(node_name) match { case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer)) case Some(model: File_Model) => Some(model.content.text) case None => read_file_content(node_name) @@ -94,7 +94,7 @@ override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { GUI_Thread.now { - Document_Model.get(name) match { + Document_Model.get_model(name) match { case Some(model: Buffer_Model) => JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) } case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text))) diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/main_plugin.scala Mon Dec 26 14:04:06 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 = @@ -113,12 +113,11 @@ val models = Document_Model.get_models() val thy_files = - resources.resolve_dependencies(models, - PIDE.editor.document_required().map((_, Position.none))) + resources.resolve_dependencies(models.values, PIDE.editor.document_required()) val aux_files = if (resources.auto_resolve) { - session.stable_tip_version(models) match { + session.stable_tip_version(models.values) match { case Some(version) => resources.undefined_blobs(version) case None => delay_load.invoke(); Nil } @@ -236,7 +235,7 @@ def init_view(buffer: Buffer, text_area: JEditTextArea): Unit = GUI_Thread.now { JEdit_Lib.buffer_lock(buffer) { - Document_Model.get(buffer) match { + Document_Model.get_model(buffer) match { case Some(model) => Document_View.init(model, text_area) case None => } diff -r b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/text_overview.scala Mon Dec 26 14:04:06 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 b61ad889dffa -r 2735b11a3de8 src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Mon Dec 26 13:54:07 2022 +0100 +++ b/src/Tools/jEdit/src/text_structure.scala Mon Dec 26 14:04:06 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")