src/Pure/ML/ml_syntax.scala
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66782 193c31b79a33
child 67493 c4e9e0c50487
permissions -rw-r--r--
more robust sorted_entries;
     1 /*  Title:      Pure/ML/ml_syntax.scala
     2     Author:     Makarius
     3 
     4 Concrete ML syntax for basic values.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object ML_Syntax
    11 {
    12   /* int */
    13 
    14   private def signed_int(s: String): String =
    15     if (s(0) == '-') "~" + s.substring(1) else s
    16 
    17   def print_int(i: Int): String = signed_int(Value.Int(i))
    18   def print_long(i: Long): String = signed_int(Value.Long(i))
    19 
    20 
    21   /* string */
    22 
    23   private def print_byte(c: Byte): String =
    24     c match {
    25       case 34 => "\\\""
    26       case 92 => "\\\\"
    27       case 9 => "\\t"
    28       case 10 => "\\n"
    29       case 12 => "\\f"
    30       case 13 => "\\r"
    31       case _ =>
    32         if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
    33         else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
    34         else if (c < 127) Symbol.ascii(c.toChar)
    35         else "\\" + Library.signed_string_of_int(c)
    36     }
    37 
    38   private def print_symbol(s: Symbol.Symbol): String =
    39     if (s.startsWith("\\<")) s
    40     else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
    41 
    42   def print_string_bytes(str: String): String =
    43     quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
    44 
    45   def print_string_symbols(str: String): String =
    46     quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
    47 
    48 
    49   /* pair */
    50 
    51   def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
    52     "(" + f(pair._1) + ", " + g(pair._2) + ")"
    53 
    54 
    55   /* list */
    56 
    57   def print_list[A](f: A => String)(list: List[A]): String =
    58     "[" + commas(list.map(f)) + "]"
    59 }