equal
deleted
inserted
replaced
21 |
21 |
22 /* concrete syntax */ |
22 /* concrete syntax */ |
23 |
23 |
24 def string(s: String): Script = |
24 def string(s: String): Script = |
25 { |
25 { |
26 val quote = if (s.contains('"')) '\'' else '"' |
26 def err(c: Char): Nothing = |
|
27 error("Bad character \\u" + String.format(Locale.ROOT, "%04x", new Integer(c)) + |
|
28 " in fontforge string " + quote(s)) |
27 |
29 |
28 def err(c: Char): Nothing = |
30 val q = if (s.contains('"')) '\'' else '"' |
29 error("Bad character in fontforge string: \\u" + |
|
30 String.format(Locale.ROOT, "%04x", new Integer(c))) |
|
31 |
31 |
32 def escape(c: Char): String = |
32 def escape(c: Char): String = |
33 { |
33 { |
34 if (c == '\u0000' || c == '\r' || c == quote) err(c) |
34 if (c == '\u0000' || c == '\r' || c == q) err(c) |
35 else if (c == '\n') "\\n" |
35 else if (c == '\n') "\\n" |
36 else if (c == '\\') "\\\\" |
36 else if (c == '\\') "\\\\" |
37 else c.toString |
37 else c.toString |
38 } |
38 } |
39 |
39 |
40 if (s.nonEmpty && s(0) == '\\') err('\\') |
40 if (s.nonEmpty && s(0) == '\\') err('\\') |
41 s.iterator.map(escape(_)).mkString(quote.toString, "", quote.toString) |
41 s.iterator.map(escape(_)).mkString(q.toString, "", q.toString) |
42 } |
42 } |
43 |
43 |
44 |
44 |
45 /* execute process */ |
45 /* execute process */ |
46 |
46 |