# HG changeset patch
# User wenzelm
# Date 1458990733 -3600
# Node ID fe3d504488336a1cba664e3fec67e5bd9996c6df
# Parent  96f20d90c9894e3b720d4eda416e5e408d266f66
more operations;

diff -r 96f20d90c989 -r fe3d50448833 src/Pure/ML/ml_syntax.scala
--- 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)) + "]"
 }