# HG changeset patch
# User wenzelm
# Date 1730754320 -3600
# Node ID 0cdd6729a962f26eedfaf4de5852d14367c1559e
# Parent  33e39b9bc4613b42597b7068a74eea5b2bed3124
clarified modules;

diff -r 33e39b9bc461 -r 0cdd6729a962 src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Mon Nov 04 21:54:34 2024 +0100
+++ b/src/Pure/General/codepoint.scala	Mon Nov 04 22:05:20 2024 +0100
@@ -25,4 +25,9 @@
   def iterator(s: String): Iterator[Int] = new Iterator_Offset(s, (c, _) => c)
 
   def length(s: String): Int = iterator(s).length
+
+  object Metric extends Pretty.Metric {
+    val unit = 1.0
+    def apply(s: String): Double = length(s).toDouble
+  }
 }
diff -r 33e39b9bc461 -r 0cdd6729a962 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Mon Nov 04 21:54:34 2024 +0100
+++ b/src/Pure/General/pretty.scala	Mon Nov 04 22:05:20 2024 +0100
@@ -53,11 +53,6 @@
     def apply(s: String): Double
   }
 
-  object Default_Metric extends Metric {
-    val unit = 1.0
-    def apply(s: String): Double = Codepoint.length(s).toDouble
-  }
-
 
   /* markup trees with physical blocks and breaks */
 
@@ -155,7 +150,7 @@
   def formatted(input: XML.Body,
     margin: Double = default_margin,
     breakgain: Double = default_breakgain,
-    metric: Metric = Default_Metric
+    metric: Metric = Codepoint.Metric
   ): XML.Body = {
     val emergencypos = (margin / 2).round.toInt
 
@@ -225,7 +220,7 @@
   def string_of(input: XML.Body,
     margin: Double = default_margin,
     breakgain: Double = default_breakgain,
-    metric: Metric = Default_Metric,
+    metric: Metric = Codepoint.Metric,
     pure: Boolean = false
   ): String = {
     output_content(pure, formatted(input, margin = margin, breakgain = breakgain, metric = metric))
diff -r 33e39b9bc461 -r 0cdd6729a962 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Nov 04 21:54:34 2024 +0100
+++ b/src/Pure/PIDE/protocol.scala	Mon Nov 04 22:05:20 2024 +0100
@@ -184,7 +184,7 @@
     pos: Position.T = Position.none,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
-    metric: Pretty.Metric = Pretty.Default_Metric
+    metric: Pretty.Metric = Codepoint.Metric
   ): String = {
     val text1 = if (heading) "\n" + message_heading(elem, pos) + ":\n" else ""