--- a/src/Pure/ML/ml_syntax.scala Thu Mar 24 16:10:18 2016 +0100
+++ b/src/Pure/ML/ml_syntax.scala Sat Mar 26 12:12:13 2016 +0100
@@ -9,6 +9,17 @@
object ML_Syntax
{
+ /* int */
+
+ private def signed_int(sign: Boolean, s: String): String =
+ if (sign) { assert(s(0) == '-'); "~" + s.substring(1) } else s
+
+ def print_int(i: Int): String = signed_int(i < 0, Properties.Value.Int(i))
+ def print_long(i: Long): String = signed_int(i < 0, Properties.Value.Long(i))
+
+
+ /* string */
+
private def print_chr(c: Byte): String =
c match {
case 34 => "\\\""
@@ -34,6 +45,9 @@
def print_string0(str: String): String =
quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+
+ /* list */
+
def print_list[A](f: A => String)(list: List[A]): String =
"[" + commas(list.map(f)) + "]"
}