Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified YXML.detect;
authorwenzelm
Tue, 12 Jul 2011 19:49:35 +0200
changeset 43782 834de29572d5
parent 43781 d43e5f79bdc2
child 43783 ef45eaf2775f
clarified YXML.detect;
src/Pure/General/yxml.ML file | annotate | diff | comparison | revisions
src/Pure/General/yxml.scala file | annotate | diff | comparison | revisions 
--- 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 *)
--- 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 (!?)
isabelle