| changeset 80486 | 24290f18ceb1 |
| parent 80480 | 972f7a4cdc0e |
| child 80487 | e25c6d4c219c |
--- a/src/Pure/PIDE/yxml.scala Wed Jul 03 10:07:39 2024 +0200 +++ b/src/Pure/PIDE/yxml.scala Wed Jul 03 10:09:59 2024 +0200 @@ -20,9 +20,6 @@ val X = X_byte.toChar val Y = Y_byte.toChar - val is_X: Char => Boolean = _ == X - val is_Y: Char => Boolean = _ == Y - val X_string: String = X.toString val Y_string: String = Y.toString val XY_string: String = X_string + Y_string