author | wenzelm |
Sat, 23 Aug 2008 17:55:26 +0200 | |
changeset 27954 | 4558d93e83b7 |
parent 27953 | b2003c98897c |
child 27955 | 4c32c5e75eca |
--- a/src/Pure/Tools/isabelle_syntax.scala Sat Aug 23 17:22:54 2008 +0200 +++ b/src/Pure/Tools/isabelle_syntax.scala Sat Aug 23 17:55:26 2008 +0200 @@ -18,6 +18,7 @@ result.append("\"") for (c <- str) { if (c < 32 || c == '\\' || c == '\"') { + result.append("\\") if (c < 10) result.append('0') if (c < 100) result.append('0') result.append(c.asInstanceOf[Int].toString)