author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 72034 | 452073b64f28 |
child 77122 | 25a497bb7b0b |
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 |
||
75393 | 10 |
object ML_Syntax { |
72034 | 11 |
/* numbers */ |
62709 | 12 |
|
72034 | 13 |
private def signed(s: String): String = |
62717 | 14 |
if (s(0) == '-') "~" + s.substring(1) else s |
62709 | 15 |
|
72034 | 16 |
def print_int(x: Int): String = signed(Value.Int(x)) |
17 |
def print_long(x: Long): String = signed(Value.Long(x)) |
|
18 |
def print_double(x: Double): String = signed(Value.Double(x)) |
|
62709 | 19 |
|
20 |
||
21 |
/* string */ |
|
22 |
||
66782 | 23 |
private def print_byte(c: Byte): String = |
62528 | 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 |
||
66782 | 38 |
private def print_symbol(s: Symbol.Symbol): String = |
62528 | 39 |
if (s.startsWith("\\<")) s |
71601 | 40 |
else UTF8.bytes(s).iterator.map(print_byte).mkString |
62528 | 41 |
|
66782 | 42 |
def print_string_bytes(str: String): String = |
71601 | 43 |
quote(UTF8.bytes(str).iterator.map(print_byte).mkString) |
62528 | 44 |
|
66782 | 45 |
def print_string_symbols(str: String): String = |
71601 | 46 |
quote(Symbol.iterator(str).map(print_symbol).mkString) |
62544 | 47 |
|
62709 | 48 |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
49 |
/* pair */ |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
50 |
|
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
51 |
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
|
52 |
"(" + f(pair._1) + ", " + g(pair._2) + ")" |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
53 |
|
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
63805
diff
changeset
|
54 |
|
62709 | 55 |
/* list */ |
56 |
||
62544 | 57 |
def print_list[A](f: A => String)(list: List[A]): String = |
58 |
"[" + commas(list.map(f)) + "]" |
|
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
59 |
|
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 |
/* properties */ |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
62 |
|
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
63 |
def print_properties(props: Properties.T): String = |
71601 | 64 |
print_list(print_pair(print_string_bytes, print_string_bytes))(props) |
62528 | 65 |
} |