Isabelle string syntax allows literal control characters;
authorwenzelm
Tue, 12 Jul 2011 11:45:13 +0200
changeset 43770 88b1b883e8d8
parent 43769 beba1a87caaa
child 43771 fc524449f511
Isabelle string syntax allows literal control characters;
src/Pure/System/isabelle_syntax.scala
--- 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)