# HG changeset patch
# User wenzelm
# Date 1731087273 -3600
# Node ID 4e9873629bffd1825aea83d7bae30ae8abbca727
# Parent  c519a14bd3f6c5f412ef350f79c48bf1c9b3e818
clarified signature;

diff -r c519a14bd3f6 -r 4e9873629bff src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Nov 08 16:57:48 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Nov 08 18:34:33 2024 +0100
@@ -388,8 +388,8 @@
 
   def text(source: String): Command = unparsed(source)
 
-  def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
-    unparsed(XML.content(body), id = id, results = results,
+  def rich_text(body: XML.Body = Nil, results: Results = Results.empty): Command =
+    unparsed(XML.content(body), id = Document_ID.make(), results = results,
       markups = Markups.init(Markup_Tree.from_XML(body)))
 
 
diff -r c519a14bd3f6 -r 4e9873629bff src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Nov 08 16:57:48 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Nov 08 18:34:33 2024 +0100
@@ -25,16 +25,10 @@
   def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
     new JEdit_Rendering(snapshot, model, options)
 
-  def text(
-    snapshot: Document.Snapshot,
-    formatted_body: XML.Body,
-    results: Command.Results = Command.Results.empty
-  ): (String, JEdit_Rendering) = {
-    val command = Command.rich_text(Document_ID.make(), results, formatted_body)
-    val snippet = snapshot.snippet(command, Document.Blobs.empty)
+  def apply(snapshot: Document.Snapshot, rich_text: Command): JEdit_Rendering = {
+    val snippet = snapshot.snippet(rich_text, Document.Blobs.empty)
     val model = File_Model.init(PIDE.session)
-    val rendering = apply(snippet, model, PIDE.options.value)
-    (command.source, rendering)
+    apply(snippet, model, PIDE.options.value)
   }
 
 
diff -r c519a14bd3f6 -r 4e9873629bff src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 16:57:48 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 08 18:34:33 2024 +0100
@@ -41,7 +41,7 @@
   private var current_base_snapshot = Document.Snapshot.init
   private var current_base_results = Command.Results.empty
   private var current_rendering: JEdit_Rendering =
-    JEdit_Rendering.text(current_base_snapshot, Nil)._2
+    JEdit_Rendering(current_base_snapshot, Command.rich_text())
   private var future_refresh: Option[Future[Unit]] = None
 
   private val rich_text_area =
@@ -99,7 +99,10 @@
       future_refresh =
         Some(Future.fork {
           val (text, rendering) =
-            try { JEdit_Rendering.text(snapshot, formatted, results = results) }
+            try {
+              val rich_text = Command.rich_text(body = formatted, results = results)
+              (rich_text.source, JEdit_Rendering(snapshot, rich_text))
+            }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
           Exn.Interrupt.expose()