diff -r d898711db199 -r 24339db7d22f src/Pure/General/pretty.scala
--- 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
   }