| changeset 27954 | 4558d93e83b7 | 
| parent 27951 | 8adddc0b591f | 
| child 29140 | e7ac5bb20aed | 
--- 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)