# 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 ""