changeset 71649 | 2acdbb6ee521 |
parent 71641 | c1409b9c2b22 |
child 71684 | 5036edb025b7 |
--- 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