author | wenzelm |
Tue, 28 Aug 2018 11:28:38 +0200 | |
changeset 68828 | 7030922e91a1 |
parent 67493 | c4e9e0c50487 |
child 71601 | 97ccf48c2f0c |
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 |
{ |
|
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 |
||
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 |
66782 | 40 |
else UTF8.bytes(s).iterator.map(print_byte(_)).mkString |
62528 | 41 |
|
66782 | 42 |
def print_string_bytes(str: String): String = |
43 |
quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString) |
|
62528 | 44 |
|
66782 | 45 |
def print_string_symbols(str: String): String = |
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 = |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
66782
diff
changeset
|
64 |
print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props) |
62528 | 65 |
} |