diff -r 4646fcb59121 -r 8bbde4dba926 src/Pure/Tools/fontforge.scala --- a/src/Pure/Tools/fontforge.scala Thu Nov 22 17:34:37 2018 +0100 +++ b/src/Pure/Tools/fontforge.scala Thu Nov 22 20:23:47 2018 +0100 @@ -23,22 +23,22 @@ def string(s: String): Script = { - val quote = if (s.contains('"')) '\'' else '"' + def err(c: Char): Nothing = + error("Bad character \\u" + String.format(Locale.ROOT, "%04x", new Integer(c)) + + " in fontforge string " + quote(s)) - def err(c: Char): Nothing = - error("Bad character in fontforge string: \\u" + - String.format(Locale.ROOT, "%04x", new Integer(c))) + val q = if (s.contains('"')) '\'' else '"' def escape(c: Char): String = { - if (c == '\u0000' || c == '\r' || c == quote) err(c) + if (c == '\u0000' || c == '\r' || c == q) err(c) else if (c == '\n') "\\n" else if (c == '\\') "\\\\" else c.toString } if (s.nonEmpty && s(0) == '\\') err('\\') - s.iterator.map(escape(_)).mkString(quote.toString, "", quote.toString) + s.iterator.map(escape(_)).mkString(q.toString, "", q.toString) }