# HG changeset patch
# User wenzelm
# Date 1219847568 -7200
# Node ID 92dd3ad302b7884d1de5f3e5e5e0b3874e7eca3e
# Parent  2cc19d1d4a427c9da3e3bff8caf58451b78ada99
simplified parse_attrib (find_substring instead of space_explode);

diff -r 2cc19d1d4a42 -r 92dd3ad302b7 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Wed Aug 27 16:32:18 2008 +0200
+++ b/src/Pure/General/yxml.ML	Wed Aug 27 16:32:48 2008 +0200
@@ -101,10 +101,10 @@
 (* parsing *)
 
 fun parse_attrib s =
-  (case space_explode "=" s of
-    [] => err_attribute ()
-  | "" :: _ => err_attribute ()
-  | a :: xs => (a, space_implode "=" xs));
+  (case find_substring "=" s of
+    NONE => err_attribute ()
+  | SOME 0 => err_attribute ()
+  | SOME i => (String.substring (s, 0, i), String.extract (s, i + 1, NONE)));
 
 fun parse_chunk ["", ""] = pop
   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)