--- a/src/Pure/General/symbol.scala Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/General/symbol.scala Wed Apr 01 20:17:23 2020 +0200
@@ -23,6 +23,7 @@
/* spaces */
+ val space_char = ' '
val space = " "
private val static_spaces = space * 4000
@@ -37,6 +38,8 @@
/* ASCII characters */
+ def is_ascii_printable(c: Char): Boolean = space_char <= c && c <= '~'
+
def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
@@ -654,4 +657,23 @@
def esub_decoded: Symbol = symbols.esub_decoded
def bsup_decoded: Symbol = symbols.bsup_decoded
def esup_decoded: Symbol = symbols.esup_decoded
+
+
+ /* metric */
+
+ def is_printable(sym: Symbol): Boolean =
+ if (is_ascii(sym)) is_ascii_printable(sym(0))
+ else !is_control(sym)
+
+ object Metric extends Pretty.Metric
+ {
+ val unit = 1.0
+ def apply(str: String): Double =
+ (for (s <- iterator(str)) yield {
+ val sym = encode(s)
+ if (sym.startsWith("\\<long") || sym.startsWith("\\<Long")) 2
+ else if (is_printable(sym)) 1
+ else 0
+ }).sum
+ }
}