# HG changeset patch
# User wenzelm
# Date 1244231708 -7200
# Node ID 40f815edbde44e01699638669b14b6d92f3da845
# Parent  b8267feaf342b5a7e06ddc08fbd593ac4faf125c
removed obsolete YXML/XML.detect;

diff -r b8267feaf342 -r 40f815edbde4 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Jun 05 17:01:02 2009 +0200
+++ b/src/Pure/General/xml.ML	Fri Jun 05 21:55:08 2009 +0200
@@ -11,7 +11,6 @@
       Elem of string * attributes * tree list
     | Text of string
   val add_content: tree -> Buffer.T -> Buffer.T
-  val detect: string -> bool
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
@@ -43,7 +42,6 @@
 
 (** string representation **)
 
-val detect = String.isPrefix "<?xml";
 val header = "<?xml version=\"1.0\"?>\n";
 
 
diff -r b8267feaf342 -r 40f815edbde4 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Fri Jun 05 17:01:02 2009 +0200
+++ b/src/Pure/General/yxml.ML	Fri Jun 05 21:55:08 2009 +0200
@@ -15,7 +15,6 @@
 
 signature YXML =
 sig
-  val detect: string -> bool
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
   val string_of: XML.tree -> string
@@ -35,8 +34,6 @@
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
-val detect = String.isPrefix XY;
-
 
 (* output *)
 
diff -r b8267feaf342 -r 40f815edbde4 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Fri Jun 05 17:01:02 2009 +0200
+++ b/src/Pure/General/yxml.scala	Fri Jun 05 21:55:08 2009 +0200
@@ -18,12 +18,6 @@
   private val X_string = X.toString
   private val Y_string = Y.toString
 
-  def detect(source: CharSequence) = {
-    source.length >= 2 &&
-    source.charAt(0) == X &&
-    source.charAt(1) == Y
-  }
-
 
   /* iterate over chunks (resembles space_explode in ML) */