# HG changeset patch
# User wenzelm
# Date 1719994487 -7200
# Node ID e25c6d4c219cff61eab7f4105ec739a5c2885324
# Parent  24290f18ceb170274f9b954eb8d62b180a3d204b
clarified signature;

diff -r 24290f18ceb1 -r e25c6d4c219c src/Pure/Isar/outer_syntax.scala
--- 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'
diff -r 24290f18ceb1 -r e25c6d4c219c src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Wed Jul 03 10:09:59 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Wed Jul 03 10:14:47 2024 +0200
@@ -17,15 +17,15 @@
   val X_byte: Byte = 5
   val Y_byte: Byte = 6
 
-  val X = X_byte.toChar
-  val Y = Y_byte.toChar
+  val X_char: Char = X_byte.toChar
+  val Y_char: Char = Y_byte.toChar
 
-  val X_string: String = X.toString
-  val Y_string: String = Y.toString
+  val X_string: String = X_char.toString
+  val Y_string: String = Y_char.toString
   val XY_string: String = X_string + Y_string
   val XYX_string: String = XY_string + X_string
 
-  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
+  def detect(s: String): Boolean = s.exists(c => c == X_char || c == Y_char)
   def detect_elem(s: String): Boolean = s.startsWith(XY_string)
 
 
@@ -105,12 +105,12 @@
 
   class Source_String(source: String) extends Source {
     override def is_empty: Boolean = source.isEmpty
-    override def is_X: Boolean = source.length == 1 && source(0) == X
-    override def is_Y: Boolean = source.length == 1 && source(0) == Y
+    override def is_X: Boolean = source.length == 1 && source(0) == X_char
+    override def is_Y: Boolean = source.length == 1 && source(0) == Y_char
     override def iterator_X: Iterator[Source] =
-      Library.separated_chunks(X, source).map(Source.apply)
+      Library.separated_chunks(X_char, source).map(Source.apply)
     override def iterator_Y: Iterator[Source] =
-      Library.separated_chunks(Y, source).map(Source.apply)
+      Library.separated_chunks(Y_char, source).map(Source.apply)
     override def text: String = source
   }