src/Pure/PIDE/yxml.scala

--- a/src/Pure/PIDE/yxml.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/yxml.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -21,10 +21,10 @@
   val is_X = (c: Char) => c == X
   val is_Y = (c: Char) => c == Y
 
-  val X_string = X.toString
-  val Y_string = Y.toString
-  val XY_string = X_string + Y_string
-  val XYX_string = XY_string + X_string
+  val X_string: String = X.toString
+  val Y_string: String = Y.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_elem(s: String): Boolean = s.startsWith(XY_string)