62528
|
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 |
{
|
62709
|
12 |
/* int */
|
|
13 |
|
62717
|
14 |
private def signed_int(s: String): String =
|
|
15 |
if (s(0) == '-') "~" + s.substring(1) else s
|
62709
|
16 |
|
63805
|
17 |
def print_int(i: Int): String = signed_int(Value.Int(i))
|
|
18 |
def print_long(i: Long): String = signed_int(Value.Long(i))
|
62709
|
19 |
|
|
20 |
|
|
21 |
/* string */
|
|
22 |
|
62528
|
23 |
private def print_chr(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 |
def print_char(s: Symbol.Symbol): String =
|
|
39 |
if (s.startsWith("\\<")) s
|
|
40 |
else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
|
|
41 |
|
|
42 |
def print_string(str: String): String =
|
|
43 |
quote(Symbol.iterator(str).map(print_char(_)).mkString)
|
|
44 |
|
62638
|
45 |
def print_string0(str: String): String =
|
62528
|
46 |
quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
|
62544
|
47 |
|
62709
|
48 |
|
|
49 |
/* list */
|
|
50 |
|
62544
|
51 |
def print_list[A](f: A => String)(list: List[A]): String =
|
|
52 |
"[" + commas(list.map(f)) + "]"
|
62528
|
53 |
}
|