clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;

--- 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()
     }

--- 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)
 }

--- 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)
   }

--- 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 {