--- 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) */