# HG changeset patch
# User wenzelm
# Date 1585765043 -7200
# Node ID 2acdbb6ee521a789d139ce55a17591da4641ae17
# Parent  12c3fe42b2a8c2007e58dd321fb33eebd862614d
pretty formatting as in Isabelle/ML;

diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/General/symbol.ML	Wed Apr 01 20:17:23 2020 +0200
@@ -501,10 +501,9 @@
 (* length *)
 
 fun sym_len s =
-  if not (is_printable s) then (0: int)
-  else if String.isPrefix "\092<long" s then 2
-  else if String.isPrefix "\092<Long" s then 2
-  else 1;
+  if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
+  else if is_printable s then 1
+  else 0;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Pure/General/symbol.scala
--- 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
+  }
 }
diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 01 20:17:23 2020 +0200
@@ -169,9 +169,15 @@
   def is_exported(msg: XML.Tree): Boolean =
     is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
 
-  def message_text(body: XML.Body, margin: Double = Pretty.default_margin): String =
+  def message_text(body: XML.Body,
+    margin: Double = Pretty.default_margin,
+    breakgain: Double = Pretty.default_breakgain,
+    metric: Pretty.Metric = Pretty.Default_Metric): String =
   {
-    val text = Pretty.string_of(Protocol_Message.expose_no_reports(body), margin = margin)
+    val text =
+      Pretty.string_of(Protocol_Message.expose_no_reports(body),
+        margin = margin, breakgain = breakgain, metric = metric)
+
     if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text)
     else if (is_message(is_error, body)) Output.error_prefix(text)
     else text
diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/PIDE/prover.scala	Wed Apr 01 20:17:23 2020 +0200
@@ -45,7 +45,7 @@
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
-        else Pretty.string_of(message.body)
+        else Pretty.string_of(message.body, metric = Symbol.Metric)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 20:17:23 2020 +0200
@@ -161,8 +161,8 @@
     {
       val errors =
         try {
-          XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)).
-            map(err => Pretty.string_of(Protocol_Message.expose_no_reports(err)))
+          for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text))) yield
+            Pretty.string_of(Protocol_Message.expose_no_reports(err), metric = Symbol.Metric)
         }
         catch { case ERROR(err) => List(err) }
       build_session_errors.fulfill(errors)
@@ -269,7 +269,8 @@
                   stdout ++= Symbol.encode(XML.content(message))
                 }
                 else if (Protocol.is_exported(message)) {
-                  messages += Symbol.encode(Protocol.message_text(List(message)))
+                  messages +=
+                    Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))
                 }
               case _ =>
             }
diff -r 12c3fe42b2a8 -r 2acdbb6ee521 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 01 18:36:58 2020 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 01 20:17:23 2020 +0200
@@ -345,7 +345,7 @@
     output_text(XML.content(xml))
 
   def output_pretty(body: XML.Body, margin: Int): String =
-    output_text(Pretty.string_of(body, margin = margin))
+    output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
   def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin)
   def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)