src/Pure/ML/ml_syntax.scala
changeset 62709 fe3d50448833
parent 62638 751cf9f3d433
child 62717 8adf274f5988
     1.1 --- a/src/Pure/ML/ml_syntax.scala	Thu Mar 24 16:10:18 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.scala	Sat Mar 26 12:12:13 2016 +0100
     1.3 @@ -9,6 +9,17 @@
     1.4  
     1.5  object ML_Syntax
     1.6  {
     1.7 +  /* int */
     1.8 +
     1.9 +  private def signed_int(sign: Boolean, s: String): String =
    1.10 +    if (sign) { assert(s(0) == '-'); "~" + s.substring(1) } else s
    1.11 +
    1.12 +  def print_int(i: Int): String = signed_int(i < 0, Properties.Value.Int(i))
    1.13 +  def print_long(i: Long): String = signed_int(i < 0, Properties.Value.Long(i))
    1.14 +
    1.15 +
    1.16 +  /* string */
    1.17 +
    1.18    private def print_chr(c: Byte): String =
    1.19      c match {
    1.20        case 34 => "\\\""
    1.21 @@ -34,6 +45,9 @@
    1.22    def print_string0(str: String): String =
    1.23      quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
    1.24  
    1.25 +
    1.26 +  /* list */
    1.27 +
    1.28    def print_list[A](f: A => String)(list: List[A]): String =
    1.29      "[" + commas(list.map(f)) + "]"
    1.30  }