src/Pure/Tools/isabelle_syntax.scala

 
   def append_string(str: String, result: StringBuilder) = {
     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)
       }
       else result.append(c)