--- a/src/Pure/General/space.scala Sat Jan 28 16:08:43 2023 +0100
+++ b/src/Pure/General/space.scala Sat Jan 28 16:20:44 2023 +0100
@@ -39,7 +39,7 @@
def PiB: Double = TiB / 1024
def EiB: Double = PiB / 1024
- override def toString: String = bytes.toString
+ override def toString: String = Value.Long(bytes)
def print: String = {
@tailrec def print_unit(x: Double, units: List[String]): String =
--- a/src/Pure/ML/ml_syntax.scala Sat Jan 28 16:08:43 2023 +0100
+++ b/src/Pure/ML/ml_syntax.scala Sat Jan 28 16:20:44 2023 +0100
@@ -29,10 +29,10 @@
case 12 => "\\f"
case 13 => "\\r"
case _ =>
- if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
+ if (c < 0) "\\" + Value.Int(256 + c)
else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
else if (c < 127) Symbol.ascii(c.toChar)
- else "\\" + Library.signed_string_of_int(c)
+ else "\\" + Value.Int(c)
}
private def print_symbol(s: Symbol.Symbol): String =