# HG changeset patch
# User wenzelm
# Date 1674919244 -3600
# Node ID 25a497bb7b0b04bf6b781ffa9f8e9a77aa6c8d3c
# Parent  ceee2a01322eb7f4dbd189f8dd912a88d444648e
tuned;

diff -r ceee2a01322e -r 25a497bb7b0b src/Pure/General/space.scala
--- 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 =
diff -r ceee2a01322e -r 25a497bb7b0b src/Pure/ML/ml_syntax.scala
--- 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 =