# HG changeset patch
# User wenzelm
# Date 1731239798 -3600
# Node ID 8c1680ac41600a14cab46d18bbcfdec10c452bdd
# Parent  d25a241502c1b2724ce01cab33fc61118843612a
clarified signature and data storage: incremental lazy values;

diff -r d25a241502c1 -r 8c1680ac4160 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:33:20 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:56:38 2024 +0100
@@ -26,14 +26,11 @@
 
   /* format */
 
-  def command(
-    body: XML.Body = Nil,
-    id: Document_ID.Command = Document_ID.none,
-    results: Command.Results = Command.Results.empty
-  ): Command = {
-    val source = XML.content(body)
-    val markups = Command.Markups.init(Markup_Tree.from_XML(body))
-    Command.unparsed(source, id = id, results = results, markups = markups)
+  sealed case class Formatted(id: Document_ID.Generic, body: XML.Body, results: Command.Results) {
+    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)))
   }
 
   def format(
@@ -41,14 +38,14 @@
     margin: Double,
     metric: Font_Metric,
     results: Command.Results
-  ) : List[Command] = {
-    val result = new mutable.ListBuffer[Command]
+  ) : List[Formatted] = {
+    val result = new mutable.ListBuffer[Formatted]
     for (msg <- msgs) {
-      if (result.nonEmpty) {
-        result += command(body = Pretty.Separator, id = Document_ID.make())
-      }
+      if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator, Command.Results.empty)
+
+      val id = Protocol_Message.get_serial(msg)
       val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
-      result += command(body = body, id = Protocol_Message.get_serial(msg))
+      result += Formatted(id, body, results)
 
       Exn.Interrupt.expose()
     }
diff -r d25a241502c1 -r 8c1680ac4160 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Nov 10 12:33:20 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Nov 10 12:56:38 2024 +0100
@@ -25,10 +25,10 @@
   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[Command]): JEdit_Rendering = {
+  def apply(snapshot: Document.Snapshot, rich_texts: List[Rich_Text.Formatted]): JEdit_Rendering = {
     val snapshot1 =
       if (rich_texts.isEmpty) snapshot
-      else snapshot.snippet(rich_texts, Document.Blobs.empty)
+      else snapshot.snippet(rich_texts.map(_.command), Document.Blobs.empty)
     val model = File_Model.init(PIDE.session)
     apply(snapshot1, model, PIDE.options.value)
   }
diff -r d25a241502c1 -r 8c1680ac4160 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 12:33:20 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 12:56:38 2024 +0100
@@ -95,11 +95,11 @@
       future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
-          val (text, rendering) =
+          val (rich_texts, rendering) =
             try {
               val rich_texts = Rich_Text.format(output, margin, metric, results)
               val rendering = JEdit_Rendering(snapshot, rich_texts)
-              (Command.full_source(rich_texts), rendering)
+              (rich_texts, rendering)
             }
             catch {
               case exn: Throwable if !Exn.is_interrupt(exn) =>
@@ -120,7 +120,7 @@
               JEdit_Lib.buffer_edit(getBuffer) {
                 rich_text_area.active_reset()
                 getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
-                JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text))
+                JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(rich_texts.map(_.text).mkString))
                 setCaretPosition(0)
               }
             }