more accurate Default_Metric;

--- a/src/Pure/General/pretty.scala	Mon Sep 02 22:41:23 2024 +0200
+++ b/src/Pure/General/pretty.scala	Wed Sep 04 12:50:52 2024 +0200
@@ -51,7 +51,7 @@
 
   object Default_Metric extends Metric {
     val unit = 1.0
-    def apply(s: String): Double = s.length.toDouble
+    def apply(s: String): Double = Codepoint.length(s).toDouble
   }