1 /* Title: Pure/Tools/isabelle_syntax.scala |
|
2 Author: Makarius |
|
3 |
|
4 Isabelle outer syntax. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object IsabelleSyntax { |
|
11 |
|
12 /* string token */ |
|
13 |
|
14 def append_string(str: String, result: StringBuilder) |
|
15 { |
|
16 result.append("\"") |
|
17 for (c <- str) { |
|
18 if (c < 32 || c == '\\' || c == '\"') { |
|
19 result.append("\\") |
|
20 if (c < 10) result.append('0') |
|
21 if (c < 100) result.append('0') |
|
22 result.append(c.asInstanceOf[Int].toString) |
|
23 } |
|
24 else result.append(c) |
|
25 } |
|
26 result.append("\"") |
|
27 } |
|
28 |
|
29 def encode_string(str: String) = |
|
30 { |
|
31 val result = new StringBuilder(str.length + 10) |
|
32 append_string(str, result) |
|
33 result.toString |
|
34 } |
|
35 |
|
36 |
|
37 /* list */ |
|
38 |
|
39 def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A], |
|
40 result: StringBuilder) |
|
41 { |
|
42 result.append("(") |
|
43 val elems = body.elements |
|
44 if (elems.hasNext) append_elem(elems.next, result) |
|
45 while (elems.hasNext) { |
|
46 result.append(", ") |
|
47 append_elem(elems.next, result) |
|
48 } |
|
49 result.append(")") |
|
50 } |
|
51 |
|
52 def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) = |
|
53 { |
|
54 val result = new StringBuilder |
|
55 append_list(append_elem, elems, result) |
|
56 result.toString |
|
57 } |
|
58 |
|
59 |
|
60 /* properties */ |
|
61 |
|
62 def append_properties(props: List[(String, String)], result: StringBuilder) |
|
63 { |
|
64 append_list((p: (String, String), res) => |
|
65 { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result) |
|
66 } |
|
67 |
|
68 def encode_properties(props: List[(String, String)]) = |
|
69 { |
|
70 val result = new StringBuilder |
|
71 append_properties(props, result) |
|
72 result.toString |
|
73 } |
|
74 } |
|