# HG changeset patch
# User wenzelm
# Date 1731237821 -3600
# Node ID de8dbdadda76a9783405e9c48eabad32ad51d6fc
# Parent  964b85e04f1f36f3decc79eaeb43b9c5b7ad2f8d
clarified modules;

diff -r 964b85e04f1f -r de8dbdadda76 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:15:31 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Sun Nov 10 12:23:41 2024 +0100
@@ -9,6 +9,8 @@
 
 import javax.swing.JComponent
 
+import scala.collection.mutable
+
 
 object Rich_Text {
   def command(
@@ -21,6 +23,25 @@
     Command.unparsed(source, id = id, results = results, markups = markups)
   }
 
+  def format(
+    msgs: List[XML.Elem],
+    margin: Double,
+    metric: Font_Metric,
+    results: Command.Results
+  ) : List[Command] = {
+    val result = new mutable.ListBuffer[Command]
+    for (msg <- msgs) {
+      if (result.nonEmpty) {
+        result += command(body = Pretty.Separator, id = Document_ID.make())
+      }
+      val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
+      result += command(body = body, id = Markup.Serial.get(msg.markup.properties))
+
+      Exn.Interrupt.expose()
+    }
+    result.toList
+  }
+
   def make_margin(metric: Font_Metric, margin: Int, limit: Int = -1): Int = {
     val m = (margin * metric.average).toInt
     (if (limit < 0) m else m min limit) max 20
diff -r 964b85e04f1f -r de8dbdadda76 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 12:15:31 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 10 12:23:41 2024 +0100
@@ -18,7 +18,6 @@
 
 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}
@@ -28,27 +27,6 @@
 import org.gjt.sp.util.{SyntaxUtilities, Log}
 
 
-object Pretty_Text_Area {
-  def format_rich_texts(
-    output: List[XML.Elem],
-    margin: Double,
-    metric: Font_Metric,
-    results: Command.Results
-  ): List[Command] = {
-    val result = new mutable.ListBuffer[Command]
-    for (msg <- output) {
-      if (result.nonEmpty) {
-        result += Rich_Text.command(body = Pretty.Separator, id = Document_ID.make())
-      }
-      val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
-      result += Rich_Text.command(body = body, id = Markup.Serial.get(msg.markup.properties))
-
-      Exn.Interrupt.expose()
-    }
-    result.toList
-  }
-}
-
 class Pretty_Text_Area(
   view: View,
   close_action: () => Unit = () => (),
@@ -119,7 +97,7 @@
         Some(Future.fork {
           val (text, rendering) =
             try {
-              val rich_texts = Pretty_Text_Area.format_rich_texts(output, margin, metric, results)
+              val rich_texts = Rich_Text.format(output, margin, metric, results)
               val rendering = JEdit_Rendering(snapshot, rich_texts)
               (Command.full_source(rich_texts), rendering)
             }