clarified YXML.detect;
authorwenzelm
Tue Jul 12 19:49:35 2011 +0200 (2011-07-12)
changeset 43782834de29572d5
parent 43781 d43e5f79bdc2
child 43783 ef45eaf2775f
clarified YXML.detect;
src/Pure/General/yxml.ML
src/Pure/General/yxml.scala
     1.1 --- a/src/Pure/General/yxml.ML	Tue Jul 12 19:47:40 2011 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Tue Jul 12 19:49:35 2011 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  val XY = X ^ Y;
     1.5  val XYX = XY ^ X;
     1.6  
     1.7 -val detect = exists_string (fn s => s = X);
     1.8 +val detect = exists_string (fn s => s = X orelse s = Y);
     1.9  
    1.10  
    1.11  (* output *)
     2.1 --- a/src/Pure/General/yxml.scala	Tue Jul 12 19:47:40 2011 +0200
     2.2 +++ b/src/Pure/General/yxml.scala	Tue Jul 12 19:49:35 2011 +0200
     2.3 @@ -19,6 +19,8 @@
     2.4    val X_string = X.toString
     2.5    val Y_string = Y.toString
     2.6  
     2.7 +  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
     2.8 +
     2.9  
    2.10    /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
    2.11