changeset 43770 | 88b1b883e8d8 |
parent 36011 | 3ff725ac13a4 |
--- a/src/Pure/System/isabelle_syntax.scala Tue Jul 12 11:19:42 2011 +0200 +++ b/src/Pure/System/isabelle_syntax.scala Tue Jul 12 11:45:13 2011 +0200 @@ -15,8 +15,8 @@ { result.append("\"") for (c <- str) { - if (c < 32 || c == '\\' || c == '\"') { - result.append("\\") + if ((c < 32 && c != 5 && c != 6) || c == '\\' || c == '\"') { + result.append("\\0") if (c < 10) result.append('0') if (c < 100) result.append('0') result.append(c.asInstanceOf[Int].toString)