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
+  }
 }