1.1 --- a/src/Pure/General/xml.ML	Sat Jul 23 17:22:28 2011 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Sat Jul 23 20:11:18 2011 +0200
     1.3 @@ -183,6 +183,10 @@
     1.4  val parse_optional_text =
     1.5    Scan.optional (parse_chars >> (single o Text)) [];
     1.6  
     1.7 +fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
     1.8 +fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
     1.9 +val parse_name = Scan.one name_start_char ::: Scan.many name_char;
    1.10 +
    1.11  in
    1.12  
    1.13  val parse_comments =
    1.14 @@ -200,13 +204,14 @@
    1.15        @@@ parse_optional_text) >> flat)) xs
    1.16  
    1.17  and parse_element xs =
    1.18 -  ($$ "<" |-- Symbol.scan_id --
    1.19 -    Scan.repeat (blanks |-- parse_att) --| blanks :-- (fn (s, _) =>
    1.20 +  ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
    1.21 +    (fn (name, _) =>
    1.22        !! (err (fn () => "Expected > or />"))
    1.23 -        (Scan.this_string "/>" >> ignored
    1.24 -         || $$ ">" |-- parse_content --|
    1.25 -            !! (err (fn () => "Expected </" ^ s ^ ">"))
    1.26 -              (Scan.this_string ("</" ^ s) --| blanks --| $$ ">"))) >> Elem) xs;
    1.27 +       ($$ "/" -- $$ ">" >> ignored ||
    1.28 +        $$ ">" |-- parse_content --|
    1.29 +          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
    1.30 +              ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
    1.31 +    >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
    1.32  
    1.33  val parse_document =
    1.34    (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)