author | wenzelm |
Mon, 29 Mar 2010 22:43:56 +0200 | |
changeset 36011 | 3ff725ac13a4 |
parent 32448 | a89f876731c5 |
child 43770 | 88b1b883e8d8 |
permissions | -rw-r--r-- |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
29571
diff
changeset
|
1 |
/* Title: Pure/System/isabelle_syntax.scala |
27951 | 2 |
Author: Makarius |
3 |
||
4 |
Isabelle outer syntax. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
29571
diff
changeset
|
10 |
object Isabelle_Syntax |
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
29571
diff
changeset
|
11 |
{ |
27951 | 12 |
/* string token */ |
13 |
||
29552 | 14 |
def append_string(str: String, result: StringBuilder) |
15 |
{ |
|
27951 | 16 |
result.append("\"") |
17 |
for (c <- str) { |
|
18 |
if (c < 32 || c == '\\' || c == '\"') { |
|
27954
4558d93e83b7
append_string: proper backslash in character escapes;
wenzelm
parents:
27951
diff
changeset
|
19 |
result.append("\\") |
27951 | 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 |
||
29552 | 29 |
def encode_string(str: String) = |
30 |
{ |
|
29571
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
31 |
val result = new StringBuilder(str.length + 10) |
27951 | 32 |
append_string(str, result) |
33 |
result.toString |
|
34 |
} |
|
35 |
||
36 |
||
29552 | 37 |
/* list */ |
38 |
||
39 |
def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A], |
|
40 |
result: StringBuilder) |
|
41 |
{ |
|
42 |
result.append("(") |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
32448
diff
changeset
|
43 |
val elems = body.iterator |
29552 | 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 |
{ |
|
29571
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
54 |
val result = new StringBuilder |
29552 | 55 |
append_list(append_elem, elems, result) |
56 |
result.toString |
|
57 |
} |
|
58 |
||
59 |
||
27951 | 60 |
/* properties */ |
61 |
||
29571
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
62 |
def append_properties(props: List[(String, String)], result: StringBuilder) |
29552 | 63 |
{ |
29571
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
64 |
append_list((p: (String, String), res) => |
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
65 |
{ append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result) |
27951 | 66 |
} |
67 |
||
29571
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
68 |
def encode_properties(props: List[(String, String)]) = |
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
69 |
{ |
ba0cf984e593
replaced java.util.Properties by plain association list;
wenzelm
parents:
29552
diff
changeset
|
70 |
val result = new StringBuilder |
27951 | 71 |
append_properties(props, result) |
72 |
result.toString |
|
73 |
} |
|
74 |
} |