tuned error;
authorwenzelm
Thu, 22 Nov 2018 20:23:47 +0100
changeset 69329 8bbde4dba926
parent 69328 4646fcb59121
child 69330 6a33b12f8573
tuned error; tuned;
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)
   }