# HG changeset patch
# User wenzelm
# Date 1750678916 -7200
# Node ID 0e0fee3599c2a3be2eaff4770d9eb4479dbfbe48
# Parent  c4964970521e20365d0c77f136033c19bca30b8f
clarified signature;

diff -r c4964970521e -r 0e0fee3599c2 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jun 23 13:41:18 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jun 23 13:41:56 2025 +0200
@@ -23,10 +23,10 @@
   def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
     new JEdit_Rendering(snapshot, model, options)
 
-  def apply(
+  def make(
     snapshot: Document.Snapshot,
-    rich_texts: List[Rich_Text.Formatted],
-    results: Command.Results
+    rich_texts: List[Rich_Text.Formatted] = Nil,
+    results: Command.Results = Command.Results.empty
   ): JEdit_Rendering = {
     val snapshot1 =
       if (rich_texts.isEmpty) snapshot
diff -r c4964970521e -r 0e0fee3599c2 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jun 23 13:41:18 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jun 23 13:41:56 2025 +0200
@@ -120,8 +120,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, Nil, Command.Results.empty)
+  private var current_rendering: JEdit_Rendering = JEdit_Rendering.make(current_base_snapshot)
 
   private val future_refresh = Synchronized[Option[Future[Unit]]](None)
   private def fork_refresh(body: => Unit): Future[Unit] =
@@ -186,7 +185,8 @@
           val (rich_texts, rendering) =
             try {
               val rich_texts = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
-              val rendering = JEdit_Rendering(snapshot, rich_texts, results)
+              val rendering =
+                JEdit_Rendering.make(snapshot, rich_texts = rich_texts, results = results)
               (rich_texts, rendering)
             }
             catch {