# HG changeset patch
# User wenzelm
# Date 1310492975 -7200
# Node ID 834de29572d517078b68a899802c5b8f13079df2
# Parent  d43e5f79bdc21600fd9b9f9805486d10a65ac96a
clarified YXML.detect;

diff -r d43e5f79bdc2 -r 834de29572d5 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Tue Jul 12 19:47:40 2011 +0200
+++ b/src/Pure/General/yxml.ML	Tue Jul 12 19:49:35 2011 +0200
@@ -52,7 +52,7 @@
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
-val detect = exists_string (fn s => s = X);
+val detect = exists_string (fn s => s = X orelse s = Y);
 
 
 (* output *)
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 (!?)