src/Pure/Isar/outer_syntax.scala
changeset 80487 e25c6d4c219c
parent 80441 c420429fdf4c
--- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 03 10:09:59 2024 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 03 10:14:47 2024 +0200
@@ -26,7 +26,7 @@
       for (s <- Symbol.iterator(str)) {
         if (s.length == 1) {
           val c = s(0)
-          if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
+          if (c < 32 && c != YXML.X_char && c != YXML.Y_char || c == '\\' || c == '"') {
             result += '\\'
             if (c < 10) result += '0'
             if (c < 100) result += '0'