slightly more standard-conformant XML parsing (see also 94033767ef9b);

--- a/src/Pure/PIDE/xml.ML	Sun Oct 16 14:48:01 2011 +0200
+++ b/src/Pure/PIDE/xml.ML	Sun Oct 16 16:56:01 2011 +0200
@@ -146,8 +146,12 @@
 
 fun ignored _ = [];
 
+fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
+fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
+val parse_name = Scan.one name_start_char ::: Scan.many name_char;
+
 val blanks = Scan.many Symbol.is_blank;
-val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
+val special = $$ "&" ^^ (parse_name >> implode) ^^ $$ ";" >> decode;
 val regular = Scan.one Symbol.is_regular;
 fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
 
@@ -159,7 +163,7 @@
   Scan.this_string "]]>";
 
 val parse_att =
-  (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
+  ((parse_name >> implode) --| (blanks -- $$ "=" -- blanks)) --
   (($$ "\"" || $$ "'") :|-- (fn s =>
     (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
 
@@ -186,10 +190,6 @@
 val parse_optional_text =
   Scan.optional (parse_chars >> (single o Text)) [];
 
-fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
-fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
-val parse_name = Scan.one name_start_char ::: Scan.many name_char;
-
 in
 
 val parse_comments =