# HG changeset patch # User wenzelm # Date 1731407527 -3600 # Node ID 85fc3b482924cf3a242cfc2a14417c811d346a38 # Parent 3585a1a77ad1d03c14d28162fe51943a6b0c9fe5 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages; diff -r 3585a1a77ad1 -r 85fc3b482924 src/Pure/GUI/rich_text.scala --- a/src/Pure/GUI/rich_text.scala Tue Nov 12 11:16:36 2024 +0100 +++ b/src/Pure/GUI/rich_text.scala Tue Nov 12 11:32:07 2024 +0100 @@ -26,26 +26,21 @@ /* format */ - sealed case class Formatted(id: Document_ID.Generic, body: XML.Body, results: Command.Results) { + sealed case class Formatted(id: Document_ID.Generic, body: XML.Body) { lazy val text: String = XML.content(body) - lazy val command: Command = - Command.unparsed(text, id = id, results = results, - markups = Command.Markups.init(Markup_Tree.from_XML(body))) + lazy val markups: Command.Markups = Command.Markups.init(Markup_Tree.from_XML(body)) + def command(results: Command.Results): Command = + Command.unparsed(text, id = id, results = results, markups = markups) } - def format( - msgs: List[XML.Elem], - margin: Double, - metric: Font_Metric, - results: Command.Results = Command.Results.empty - ) : List[Formatted] = { + def format(msgs: List[XML.Elem], margin: Double, metric: Font_Metric): List[Formatted] = { val result = new mutable.ListBuffer[Formatted] for (msg <- msgs) { - if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator, results) + if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator) val id = Protocol_Message.get_serial(msg) val body = Pretty.formatted(List(msg), margin = margin, metric = metric) - result += Formatted(id, body, results) + result += Formatted(id, body) Exn.Interrupt.expose() } diff -r 3585a1a77ad1 -r 85fc3b482924 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Nov 12 11:16:36 2024 +0100 +++ b/src/Pure/PIDE/command.scala Tue Nov 12 11:32:07 2024 +0100 @@ -478,8 +478,8 @@ def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none - val is_unparsed: Boolean = span.content.exists(_.is_unparsed) - val is_unfinished: Boolean = span.content.exists(_.is_unfinished) + lazy val is_unparsed: Boolean = span.content.exists(_.is_unparsed) + lazy val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY @@ -506,9 +506,9 @@ /* source chunks */ - val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) + lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) - val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = + lazy val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (case Exn.Res(blob) <- blobs; (_, file) <- blob.content) yield blob.chunk_file -> file)).toMap @@ -516,7 +516,7 @@ def length: Int = source.length def range: Text.Range = chunk.range - val core_range: Text.Range = + lazy val core_range: Text.Range = Text.Range(0, span.content.reverseIterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length)) @@ -600,8 +600,8 @@ /* accumulated results */ - val init_state: Command.State = + lazy val init_state: Command.State = Command.State(this, results = init_results, markups = init_markups) - val empty_state: Command.State = Command.State(this) + lazy val empty_state: Command.State = Command.State(this) } diff -r 3585a1a77ad1 -r 85fc3b482924 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Nov 12 11:16:36 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Nov 12 11:32:07 2024 +0100 @@ -25,10 +25,14 @@ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) - def apply(snapshot: Document.Snapshot, rich_texts: List[Rich_Text.Formatted]): JEdit_Rendering = { + def apply( + snapshot: Document.Snapshot, + rich_texts: List[Rich_Text.Formatted], + results: Command.Results + ): JEdit_Rendering = { val snapshot1 = if (rich_texts.isEmpty) snapshot - else snapshot.snippet(rich_texts.map(_.command), Document.Blobs.empty) + else snapshot.snippet(rich_texts.map(_.command(results)), Document.Blobs.empty) val model = File_Model.init(PIDE.session) apply(snapshot1, model, PIDE.options.value) } diff -r 3585a1a77ad1 -r 85fc3b482924 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Nov 12 11:16:36 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Nov 12 11:32:07 2024 +0100 @@ -40,7 +40,8 @@ private var current_output: List[XML.Elem] = Nil private var current_base_snapshot = Document.Snapshot.init private var current_base_results = Command.Results.empty - private var current_rendering: JEdit_Rendering = JEdit_Rendering(current_base_snapshot, Nil) + private var current_rendering: JEdit_Rendering = + JEdit_Rendering(current_base_snapshot, Nil, Command.Results.empty) private var future_refresh: Option[Future[Unit]] = None private val rich_text_area = @@ -97,8 +98,8 @@ Some(Future.fork { val (rich_texts, rendering) = try { - val rich_texts = Rich_Text.format(output, margin, metric, results = results) - val rendering = JEdit_Rendering(snapshot, rich_texts) + val rich_texts = Rich_Text.format(output, margin, metric) + val rendering = JEdit_Rendering(snapshot, rich_texts, results) (rich_texts, rendering) } catch {