author | wenzelm |
Wed, 15 Jul 2020 11:56:43 +0200 | |
changeset 72034 | 452073b64f28 |
parent 71601 | 97ccf48c2f0c |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
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 |
{ |
|
72034 | 12 |
/* numbers */ |
62709 | 13 |
|
72034 | 14 |
private def signed(s: String): String = |
62717 | 15 |
if (s(0) == '-') "~" + s.substring(1) else s |
62709 | 16 |
|
72034 | 17 |
def print_int(x: Int): String = signed(Value.Int(x)) |
18 |
def print_long(x: Long): String = signed(Value.Long(x)) |
|
19 |
def print_double(x: Double): String = signed(Value.Double(x)) |
|
62709 | 20 |
|
21 |
||
22 |
/* string */ |
|
23 |
||
66782 | 24 |
private def print_byte(c: Byte): String = |
62528 | 25 |
c match { |
26 |
case 34 => "\\\"" |
|
27 |
case 92 => "\\\\" |
|
28 |
case 9 => "\\t" |
|
29 |
case 10 => "\\n" |
|
30 |
case 12 => "\\f" |
|
31 |
case 13 => "\\r" |
|
32 |
case _ => |
|
33 |
if (c < 0) "\\" + Library.signed_string_of_int(256 + c) |
|
34 |
else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar)) |
|
35 |
else if (c < 127) Symbol.ascii(c.toChar) |
|
36 |
else "\\" + Library.signed_string_of_int(c) |
|
37 |
} |
|
38 |
||
66782 | 39 |
private def print_symbol(s: Symbol.Symbol): String = |
62528 | 40 |
if (s.startsWith("\\<")) s |
71601 | 41 |
else UTF8.bytes(s).iterator.map(print_byte).mkString |
62528 | 42 |
|
66782 | 43 |
def print_string_bytes(str: String): String = |
71601 | 44 |
quote(UTF8.bytes(str).iterator.map(print_byte).mkString) |
62528 | 45 |
|
66782 | 46 |
def print_string_symbols(str: String): String = |
71601 | 47 |
quote(Symbol.iterator(str).map(print_symbol).mkString) |
62544 | 48 |
|
62709 | 49 |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
50 |
/* pair */ |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
51 |
|
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
52 |
def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String = |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
53 |
"(" + f(pair._1) + ", " + g(pair._2) + ")" |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
54 |
|
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
55 |
|
62709 | 56 |
/* list */ |
57 |
||
62544 | 58 |
def print_list[A](f: A => String)(list: List[A]): String = |
59 |
"[" + commas(list.map(f)) + "]" |
|
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
60 |
|
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
61 |
|
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
62 |
/* properties */ |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
63 |
|
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
64 |
def print_properties(props: Properties.T): String = |
71601 | 65 |
print_list(print_pair(print_string_bytes, print_string_bytes))(props) |
62528 | 66 |
} |