diff -r f8715e7c1be6 -r b979c781c2db src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/PIDE/xml.ML	Fri Oct 31 22:02:49 2014 +0100
@@ -192,8 +192,8 @@
 
 val blanks = Scan.many Symbol.is_blank;
 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);
+val regular = Scan.one Symbol.not_eof;
+fun regular_except x = Scan.one (fn c => Symbol.not_eof c andalso c <> x);
 
 val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;