--- 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>\<open>etc/build.props\<close> follows a regular Java properties
- file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
+ file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API
documentation.
--- 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 \<Rightarrow> 'b::{conditionally_complete_linorder,ordered_ab_group_add}"
+begin
+
+lemma bdd_above_uminus_image: "bdd_above ((\<lambda>x. - f x) ` A) \<longleftrightarrow> bdd_below (f ` A)"
+ by (metis bdd_above_uminus image_image)
+
+lemma bdd_below_uminus_image: "bdd_below ((\<lambda>x. - f x) ` A) \<longleftrightarrow> bdd_above (f ` A)"
+ by (metis bdd_below_uminus image_image)
+
+lemma uminus_cSUP:
+ assumes "bdd_above (f ` A)" "A \<noteq> {}"
+ shows "- (SUP x\<in>A. f x) = (INF x\<in>A. - f x)"
+proof (rule antisym)
+ show "(INF x\<in>A. - f x) \<le> - Sup (f ` A)"
+ by (metis cINF_lower cSUP_least bdd_below_uminus_image assms le_minus_iff)
+ have *: "\<And>x. x \<in>A \<Longrightarrow> f x \<le> Sup (f ` A)"
+ by (simp add: assms cSup_upper)
+ then show "- Sup (f ` A) \<le> (INF x\<in>A. - f x)"
+ by (simp add: assms cINF_greatest)
+qed
+
+end
+
+context
+ fixes f::"'a \<Rightarrow> 'b::{conditionally_complete_linorder,ordered_ab_group_add}"
+begin
+
+lemma uminus_cINF:
+ assumes "bdd_below (f ` A)" "A \<noteq> {}"
+ shows "- (INF x\<in>A. f x) = (SUP x\<in>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 \<noteq> {}"
+ shows "(SUP x\<in>A. a + f x) = a + (SUP x\<in>A. f x)" (is "?L=?R")
+proof (rule antisym)
+ have bdd: "bdd_above ((\<lambda>x. a + f x) ` A)"
+ by (metis assms bdd_above_image_mono image_image mono_add)
+ with assms show "?L \<le> ?R"
+ by (simp add: assms cSup_le_iff cSUP_upper)
+ have "\<And>x. x \<in> A \<Longrightarrow> f x \<le> (SUP x\<in>A. a + f x) - a"
+ by (simp add: bdd cSup_upper le_diff_eq)
+ with \<open>A \<noteq> {}\<close> have "\<Squnion> (f ` A) \<le> (\<Squnion>x\<in>A. a + f x) - a"
+ by (simp add: cSUP_least)
+ then show "?R \<le> ?L"
+ by (metis add.commute le_diff_eq)
+qed
+
+lemma Inf_add_eq: \<comment>\<open>you don't get a shorter proof by duality\<close>
+ assumes "bdd_below (f ` A)" "A \<noteq> {}"
+ shows "(INF x\<in>A. a + f x) = a + (INF x\<in>A. f x)" (is "?L=?R")
+proof (rule antisym)
+ show "?R \<le> ?L"
+ using assms mono_add mono_cINF by blast
+ have bdd: "bdd_below ((\<lambda>x. a + f x) ` A)"
+ by (metis add_left_mono assms(1) bdd_below.E bdd_below.I2 imageI)
+ with assms have "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> (INF x\<in>A. a + f x) - a"
+ by (simp add: cInf_lower diff_le_eq)
+ with \<open>A \<noteq> {}\<close> have "(\<Sqinter>x\<in>A. a + f x) - a \<le> \<Sqinter> (f ` A)"
+ by (simp add: cINF_greatest)
+ with assms show "?L \<le> ?R"
+ by (metis add.commute diff_le_eq)
+qed
+
+end
+
instantiation nat :: conditionally_complete_linorder
begin
--- 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 =
--- 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
--- 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 = {
--- 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
--- 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)
--- 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)
}
}
--- 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 =
--- 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 */
--- 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 */
--- 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 {
--- 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 {
--- 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))
}
--- 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 {
--- 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
--- 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 =
--- 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)
}
}
--- 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) &&
--- 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) =>
--- 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
--- 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)))
--- 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)
--- 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 =>
}
--- 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()
--- 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")