equal
deleted
inserted
replaced
22 if ("!#$&'()*+,/:;=?@[]".contains(c)) { |
22 if ("!#$&'()*+,/:;=?@[]".contains(c)) { |
23 String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt)) |
23 String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt)) |
24 } |
24 } |
25 else c.toString |
25 else c.toString |
26 |
26 |
27 def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString |
27 def escape_special(s: String): String = s.iterator.map(escape_special).mkString |
28 |
28 |
29 def escape_name(name: String): String = |
29 def escape_name(name: String): String = |
30 name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString |
30 name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString |
31 |
31 |
32 |
32 |