src/Pure/ML/ml_syntax.scala
author wenzelm
Wed Mar 16 20:50:38 2016 +0100 (2016-03-16)
changeset 62638 751cf9f3d433
parent 62544 efa178abe023
child 62709 fe3d50448833
permissions -rw-r--r--
tuned signature;
wenzelm@62528
     1
/*  Title:      Pure/ML/ml_syntax.scala
wenzelm@62528
     2
    Author:     Makarius
wenzelm@62528
     3
wenzelm@62528
     4
Concrete ML syntax for basic values.
wenzelm@62528
     5
*/
wenzelm@62528
     6
wenzelm@62528
     7
package isabelle
wenzelm@62528
     8
wenzelm@62528
     9
wenzelm@62528
    10
object ML_Syntax
wenzelm@62528
    11
{
wenzelm@62528
    12
  private def print_chr(c: Byte): String =
wenzelm@62528
    13
    c match {
wenzelm@62528
    14
      case 34 => "\\\""
wenzelm@62528
    15
      case 92 => "\\\\"
wenzelm@62528
    16
      case 9 => "\\t"
wenzelm@62528
    17
      case 10 => "\\n"
wenzelm@62528
    18
      case 12 => "\\f"
wenzelm@62528
    19
      case 13 => "\\r"
wenzelm@62528
    20
      case _ =>
wenzelm@62528
    21
        if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
wenzelm@62528
    22
        else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
wenzelm@62528
    23
        else if (c < 127) Symbol.ascii(c.toChar)
wenzelm@62528
    24
        else "\\" + Library.signed_string_of_int(c)
wenzelm@62528
    25
    }
wenzelm@62528
    26
wenzelm@62528
    27
  def print_char(s: Symbol.Symbol): String =
wenzelm@62528
    28
    if (s.startsWith("\\<")) s
wenzelm@62528
    29
    else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
wenzelm@62528
    30
wenzelm@62528
    31
  def print_string(str: String): String =
wenzelm@62528
    32
    quote(Symbol.iterator(str).map(print_char(_)).mkString)
wenzelm@62528
    33
wenzelm@62638
    34
  def print_string0(str: String): String =
wenzelm@62528
    35
    quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
wenzelm@62544
    36
wenzelm@62544
    37
  def print_list[A](f: A => String)(list: List[A]): String =
wenzelm@62544
    38
    "[" + commas(list.map(f)) + "]"
wenzelm@62528
    39
}