# HG changeset patch
# User wenzelm
# Date 1731325671 -3600
# Node ID 257ec066b36037c7c3e372a4a48ceded20506331
# Parent  ecd62f7b3644790f4269ea5f653f93bfc5e23d88
clarified signature and modules;
more basic Rich_Text.formatted_lines, assuming that elements are properly separated according to Rich_Text.format;

diff -r ecd62f7b3644 -r 257ec066b360 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Mon Nov 11 12:19:45 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Mon Nov 11 12:47:51 2024 +0100
@@ -37,7 +37,7 @@
     msgs: List[XML.Elem],
     margin: Double,
     metric: Font_Metric,
-    results: Command.Results
+    results: Command.Results = Command.Results.empty
   ) : List[Formatted] = {
     val result = new mutable.ListBuffer[Formatted]
     for (msg <- msgs) {
@@ -51,4 +51,15 @@
     }
     result.toList
   }
+
+  def formatted_lines(formatted: List[Formatted]): Int =
+    if (formatted.isEmpty) 0
+    else {
+      1 + formatted.iterator.map(form =>
+        XML.traverse_text(form.body, 0, (n, s) => n + Library.count_newlines(s))).sum
+    }
+
+  def formatted_margin(metric: Font_Metric, formatted: List[Formatted]): Double =
+    split_lines(formatted.map(_.text).mkString)
+      .foldLeft(0.0) { case (m, line) => m max metric(line) }
 }
diff -r ecd62f7b3644 -r 257ec066b360 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Mon Nov 11 12:19:45 2024 +0100
+++ b/src/Pure/PIDE/xml.scala	Mon Nov 11 12:47:51 2024 +0100
@@ -177,14 +177,6 @@
   def text_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + s.length)
   def symbol_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + Symbol.length(s))
 
-  def content_is_empty(body: Body): Boolean =
-    traverse_text(body, true, (b, s) => b && s.isEmpty)
-
-  def content_lines(body: Body): Int = {
-    val n = traverse_text(body, 0, (n, s) => n + Library.count_newlines(s))
-    if (n == 0 && content_is_empty(body)) 0 else n + 1
-  }
-
   def content(body: Body): String =
     Library.string_builder(hint = text_length(body)) { text =>
       traverse_text(body, (), (_, s) => text.append(s))
diff -r ecd62f7b3644 -r 257ec066b360 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 11 12:19:45 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Nov 11 12:47:51 2024 +0100
@@ -97,7 +97,7 @@
         Some(Future.fork {
           val (rich_texts, rendering) =
             try {
-              val rich_texts = Rich_Text.format(output, margin, metric, results)
+              val rich_texts = Rich_Text.format(output, margin, metric, results = results)
               val rendering = JEdit_Rendering(snapshot, rich_texts)
               (rich_texts, rendering)
             }
diff -r ecd62f7b3644 -r 257ec066b360 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Nov 11 12:19:45 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Nov 11 12:47:51 2024 +0100
@@ -251,14 +251,12 @@
         Rich_Text.make_margin(metric, rendering.tooltip_margin,
           limit = ((w_max - geometry.deco_width) / metric.average_width).toInt)
 
-      val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric)
-      val lines = XML.content_lines(formatted)
+      val formatted = Rich_Text.format(output, margin, metric)
+      val lines = Rich_Text.formatted_lines(formatted)
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
-        if (h <= h_max) {
-          split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
-        }
+        if (h <= h_max) Rich_Text.formatted_margin(metric, formatted)
         else margin.toDouble
       val w = (metric.unit * (margin1 + 1)).round.toInt + geometry.deco_width