Document.Snapshot: support for multiple snippet_commands;
clarified Command.rich_text: prefer explicit id, e.g. from message serial;
clarified Pretty_Text_Area.update: Protocol_Message.provide_serial;
clarified Pretty_Text_Area.format_rich_texts, with separate formatting of messages;

--- a/src/Pure/Build/build.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -764,7 +764,7 @@
 
       val doc_blobs = Document.Blobs.make(blobs)
 
-      Document.State.init.snippet(command, doc_blobs)
+      Document.State.init.snippet(List(command), doc_blobs)
     }
   }
 

--- a/src/Pure/Build/build_job.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -300,7 +300,7 @@
                 def export_text(name: String, text: String, compress: Boolean = true): Unit =
                   export_(name, List(XML.Text(text)), compress = compress)
 
-                for (command <- snapshot.snippet_command) {
+                for (command <- snapshot.snippet_commands) {
                   export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
                 }
 

--- a/src/Pure/PIDE/command.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -386,9 +386,17 @@
     new Command(id, node_name, blobs_info, span1, source1, results, markups)
   }
 
-  def rich_text(body: XML.Body = Nil, results: Results = Results.empty): Command =
-    unparsed(XML.content(body), id = Document_ID.make(), results = results,
+  def rich_text(
+    body: XML.Body = Nil,
+    id: Document_ID.Command = Document_ID.none,
+    results: Results = Results.empty
+  ): Command = {
+    unparsed(XML.content(body), id = id, results = results,
       markups = Markups.init(Markup_Tree.from_XML(body)))
+  }
+
+  def full_source(commands: Iterable[Command]): String =
+    commands.iterator.map(_.source).mkString
 
 
   /* edits and perspective */

--- a/src/Pure/PIDE/document.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -568,7 +568,7 @@
     val version: Version,
     val node_name: Node.Name,
     pending_edits: Pending_Edits,
-    val snippet_command: Option[Command]
+    val snippet_commands: List[Command]
   ) {
     override def toString: String =
       "Snapshot(node = " + node_name.node + ", version = " + version.id +
@@ -576,7 +576,7 @@
 
     def switch(name: Node.Name): Snapshot =
       if (name == node_name) this
-      else new Snapshot(state, version, name, pending_edits, None)
+      else new Snapshot(state, version, name, pending_edits, Nil)
 
 
     /* nodes */
@@ -628,27 +628,41 @@
 
     /* command as add-on snippet */
 
-    def snippet(command: Command, doc_blobs: Blobs): Snapshot = {
-      val node_name = command.node_name
+    def snippet(commands: List[Command], doc_blobs: Blobs): Snapshot = {
+      require(commands.nonEmpty, "no snippet commands")
+
+      val node_name = commands.head.node_name
+      val node_commands = Linear_Set.from(commands)
 
-      val blobs = for (a <- command.blobs_names; b <- doc_blobs.get(a)) yield a -> b
+      require(commands.forall(command => command.node_name == node_name),
+        "incoherent snippet node names")
+
+      val blobs =
+        for {
+          command <- commands
+          a <- command.blobs_names
+          b <- doc_blobs.get(a)
+        } yield a -> b
 
       val nodes0 = version.nodes
-      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
+      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(node_commands))
       val nodes2 = blobs.foldLeft(nodes1) { case (ns, (a, b)) => ns + (a -> Node.init_blob(b)) }
       val version1 = Version.make(nodes2)
 
       val edits: List[Edit_Text] =
-        List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) :::
+        List(node_name -> Node.Edits(List(Text.Edit.insert(0, Command.full_source(commands))))) :::
         blobs.map({ case (a, b) => a -> Node.Blob(b) })
 
-      val state0 = state.define_command(command)
+      val assign_update: Assign_Update =
+        commands.map(command => command.id -> List(Document_ID.make()))
+
+      val state0 = commands.foldLeft(state)(_.define_command(_))
       val state1 =
         state0.continue_history(Future.value(version), edits, Future.value(version1))
           .define_version(version1, state0.the_assignment(version))
-          .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
+          .assign(version1.id, Nil, assign_update)._2
 
-      state1.snapshot(node_name = node_name, snippet_command = Some(command))
+      state1.snapshot(node_name = node_name, snippet_commands = commands)
     }
 
 
@@ -1030,7 +1044,7 @@
             Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - id)
-          (state1.snippet(command1, doc_blobs), state1)
+          (state1.snippet(List(command1), doc_blobs), state1)
       }
 
     def assign(
@@ -1254,7 +1268,7 @@
     def snapshot(
       node_name: Node.Name = Node.Name.empty,
       pending_edits: Pending_Edits = Pending_Edits.empty,
-      snippet_command: Option[Command] = None
+      snippet_commands: List[Command] = Nil
     ): Snapshot = {
       val stable = recent_stable
       val version = stable.version.get_finished
@@ -1265,10 +1279,10 @@
           case (name, Node.Edits(es)) <- change.rev_edits
         } yield (name -> es)).foldLeft(pending_edits)(_ + _)
 
-      new Snapshot(this, version, node_name, pending_edits1, snippet_command)
+      new Snapshot(this, version, node_name, pending_edits1, snippet_commands)
     }
 
-    def snippet(command: Command, doc_blobs: Blobs): Snapshot =
-      snapshot().snippet(command, doc_blobs)
+    def snippet(commands: List[Command], doc_blobs: Blobs): Snapshot =
+      snapshot().snippet(commands, doc_blobs)
   }
 }

--- a/src/Pure/PIDE/protocol_message.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Pure/PIDE/protocol_message.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -34,6 +34,13 @@
   }
 
 
+  /* message serial */
+
+  def provide_serial(msg: XML.Elem): XML.Elem =
+    if (Markup.Serial.get(msg.markup.properties) != 0L) msg
+    else msg.copy(markup = msg.markup.update_properties(Markup.Serial(Document_ID.make())))
+
+
   /* inlined reports */
 
   val report_elements: Markup.Elements = Markup.Elements(Markup.REPORT)

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -25,10 +25,12 @@
   def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
     new JEdit_Rendering(snapshot, model, options)
 
-  def apply(snapshot: Document.Snapshot, rich_text: Command): JEdit_Rendering = {
-    val snippet = snapshot.snippet(rich_text, Document.Blobs.empty)
+  def apply(snapshot: Document.Snapshot, rich_texts: List[Command]): JEdit_Rendering = {
+    val snapshot1 =
+      if (rich_texts.isEmpty) snapshot
+      else snapshot.snippet(rich_texts, Document.Blobs.empty)
     val model = File_Model.init(PIDE.session)
-    apply(snippet, model, PIDE.options.value)
+    apply(snapshot1, model, PIDE.options.value)
   }
 
 

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 16:39:33 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Nov 09 21:34:38 2024 +0100
@@ -18,6 +18,7 @@
 
 import scala.swing.{Label, Component}
 import scala.util.matching.Regex
+import scala.collection.mutable
 
 import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
 import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
@@ -27,6 +28,24 @@
 import org.gjt.sp.util.{SyntaxUtilities, Log}
 
 
+object Pretty_Text_Area {
+  def format_rich_texts(
+    output: List[XML.Elem],
+    metric: Font_Metric,
+    results: Command.Results
+  ): List[Command] = {
+    val result = new mutable.ListBuffer[Command]
+    for (msg <- output) {
+      if (result.nonEmpty) {
+        result += Command.rich_text(body = Pretty.Separator, id = Document_ID.make())
+      }
+      val body = Pretty.formatted(List(msg), margin = metric.margin, metric = metric)
+      result += Command.rich_text(body = body, id = Markup.Serial.get(msg.markup.properties))
+    }
+    result.toList
+  }
+}
+
 class Pretty_Text_Area(
   view: View,
   close_action: () => Unit = () => (),
@@ -40,8 +59,7 @@
   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, Command.rich_text())
+  private var current_rendering: JEdit_Rendering = JEdit_Rendering(current_base_snapshot, Nil)
   private var future_refresh: Option[Future[Unit]] = None
 
   private val rich_text_area =
@@ -95,11 +113,12 @@
       future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
-          val formatted =
-            Pretty.formatted(Pretty.separate(output), margin = metric.margin, metric = metric)
-          val rich_text = Command.rich_text(body = formatted, results = results)
-          val rendering =
-            try { JEdit_Rendering(snapshot, rich_text) }
+          val (text, rendering) =
+            try {
+              val rich_texts = Pretty_Text_Area.format_rich_texts(output, metric, results)
+              val rendering = JEdit_Rendering(snapshot, rich_texts)
+              (Command.full_source(rich_texts), rendering)
+            }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
           Exn.Interrupt.expose()
 
@@ -113,7 +132,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(rich_text.source))
+                JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text))
                 setCaretPosition(0)
               }
             }
@@ -137,7 +156,7 @@
 
     current_base_snapshot = base_snapshot
     current_base_results = base_results
-    current_output = output
+    current_output = output.map(Protocol_Message.provide_serial)
     refresh()
   }