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'