author | wenzelm |
Tue, 12 Jul 2011 11:45:13 +0200 | |
changeset 43770 | 88b1b883e8d8 |
parent 43769 | beba1a87caaa |
child 43771 | fc524449f511 |
--- 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)