diff -r d43e5f79bdc2 -r 834de29572d5 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Tue Jul 12 19:47:40 2011 +0200 +++ b/src/Pure/General/yxml.scala Tue Jul 12 19:49:35 2011 +0200 @@ -19,6 +19,8 @@ val X_string = X.toString val Y_string = Y.toString + def detect(s: String): Boolean = s.exists(c => c == X || c == Y) + /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)