# HG changeset patch
# User wenzelm
# Date 1318776961 -7200
# Node ID 3216d65d8f342aa288a0df5c7d434fef1eb94ec7
# Parent  66e8a5812f413887f7e9be35c621f44287d8667a
slightly more standard-conformant XML parsing (see also 94033767ef9b);

diff -r 66e8a5812f41 -r 3216d65d8f34 src/Pure/PIDE/xml.ML
--- 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 =