1/*  Title:      Pure/ML/ml_syntax.scala
2    Author:     Makarius
3
4Concrete ML syntax for basic values.
5*/
6
7package isabelle
8
9
10object 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
60
61  /* properties */
62
63  def print_properties(props: Properties.T): String =
64    print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
65}
66