removed obsolete YXML/XML.detect;
authorwenzelm
Fri, 05 Jun 2009 21:55:08 +0200
changeset 31469 40f815edbde4
parent 31468 b8267feaf342
child 31470 01e7a8bb9e5b
child 31487 93938cafc0e6
removed obsolete YXML/XML.detect;
src/Pure/General/xml.ML
src/Pure/General/yxml.ML
src/Pure/General/yxml.scala
--- 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";
 
 
--- 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 *)
 
--- 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) */