equal
deleted
inserted
replaced
22 /* concrete syntax */ |
22 /* concrete syntax */ |
23 |
23 |
24 def string(s: String): Script = |
24 def string(s: String): Script = |
25 { |
25 { |
26 def err(c: Char): Nothing = |
26 def err(c: Char): Nothing = |
27 error("Bad character \\u" + String.format(Locale.ROOT, "%04x", new Integer(c)) + |
27 error("Bad character \\u" + String.format(Locale.ROOT, "%04x", Integer.valueOf(c)) + |
28 " in fontforge string " + quote(s)) |
28 " in fontforge string " + quote(s)) |
29 |
29 |
30 val q = if (s.contains('"')) '\'' else '"' |
30 val q = if (s.contains('"')) '\'' else '"' |
31 |
31 |
32 def escape(c: Char): String = |
32 def escape(c: Char): String = |