# HG changeset patch
# User wenzelm
# Date 1725447052 -7200
# Node ID 24339db7d22f829e276e8d8364e5824b7f734b87
# Parent  d898711db19911960f63ab1920c5326c903658c1
more accurate Default_Metric;

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
   }