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;
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@62709
    12
  /* int */
wenzelm@62709
    13
wenzelm@62717
    14
  private def signed_int(s: String): String =
wenzelm@62717
    15
    if (s(0) == '-') "~" + s.substring(1) else s
wenzelm@62709
    16
wenzelm@63805
    17
  def print_int(i: Int): String = signed_int(Value.Int(i))
wenzelm@63805
    18
  def print_long(i: Long): String = signed_int(Value.Long(i))
wenzelm@62709
    19
wenzelm@62709
    20
wenzelm@62709
    21
  /* string */
wenzelm@62709
    22
wenzelm@66782
    23
  private def print_byte(c: Byte): String =
wenzelm@62528
    24
    c match {
wenzelm@62528
    25
      case 34 => "\\\""
wenzelm@62528
    26
      case 92 => "\\\\"
wenzelm@62528
    27
      case 9 => "\\t"
wenzelm@62528
    28
      case 10 => "\\n"
wenzelm@62528
    29
      case 12 => "\\f"
wenzelm@62528
    30
      case 13 => "\\r"
wenzelm@62528
    31
      case _ =>
wenzelm@62528
    32
        if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
wenzelm@62528
    33
        else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
wenzelm@62528
    34
        else if (c < 127) Symbol.ascii(c.toChar)
wenzelm@62528
    35
        else "\\" + Library.signed_string_of_int(c)
wenzelm@62528
    36
    }
wenzelm@62528
    37
wenzelm@66782
    38
  private def print_symbol(s: Symbol.Symbol): String =
wenzelm@62528
    39
    if (s.startsWith("\\<")) s
wenzelm@66782
    40
    else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
wenzelm@62528
    41
wenzelm@66782
    42
  def print_string_bytes(str: String): String =
wenzelm@66782
    43
    quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
wenzelm@62528
    44
wenzelm@66782
    45
  def print_string_symbols(str: String): String =
wenzelm@66782
    46
    quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
wenzelm@62544
    47
wenzelm@62709
    48
wenzelm@65431
    49
  /* pair */
wenzelm@65431
    50
wenzelm@65431
    51
  def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
wenzelm@65431
    52
    "(" + f(pair._1) + ", " + g(pair._2) + ")"
wenzelm@65431
    53
wenzelm@65431
    54
wenzelm@62709
    55
  /* list */
wenzelm@62709
    56
wenzelm@62544
    57
  def print_list[A](f: A => String)(list: List[A]): String =
wenzelm@62544
    58
    "[" + commas(list.map(f)) + "]"
wenzelm@62528
    59
}