src/Pure/General/xml.ML
changeset 14863 49afb368f4be
parent 14844 a15c65e66ee9
child 14865 8b9a372b3e90
equal deleted inserted replaced
14862:a43f9e2c6332 14863:49afb368f4be
    91 val parse_att =
    91 val parse_att =
    92   Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "\"" --
    92   Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "\"" --
    93   (Scan.repeat (Scan.unless ($$ "\"")
    93   (Scan.repeat (Scan.unless ($$ "\"")
    94     (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
    94     (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
    95 
    95 
       
    96 val parse_att2 = 
       
    97   Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "'" --
       
    98   (Scan.repeat (Scan.unless ($$ "'")
       
    99     (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "'";
       
   100 
    96 val parse_comment = scan_lit "<!--" --
   101 val parse_comment = scan_lit "<!--" --
    97   Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
   102   Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
    98   scan_lit "-->";
   103   scan_lit "-->";
    99 
   104 
   100 val parse_pi = scan_lit "<?" |--
   105 val parse_pi = scan_lit "<?" |--
   111        Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) []
   116        Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) []
   112          >> op @) >> flat) >> op @) --| scan_whspc) xs
   117          >> op @) >> flat) >> op @) --| scan_whspc) xs
   113 
   118 
   114 and parse_elem xs =
   119 and parse_elem xs =
   115   ($$ "<" |-- Symbol.scan_id --
   120   ($$ "<" |-- Symbol.scan_id --
   116     Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
   121     Scan.repeat (scan_whspc |-- (parse_att || parse_att2)) --| scan_whspc :-- (fn (s, _) =>
   117       !! (err "Expected > or />")
   122       !! (err "Expected > or />")
   118         (scan_lit "/>" >> K []
   123         (scan_lit "/>" >> K []
   119          || $$ ">" |-- parse_content --|
   124          || $$ ">" |-- parse_content --|
   120             !! (err ("Expected </" ^ s ^ ">"))
   125             !! (err ("Expected </" ^ s ^ ">"))
   121               (scan_lit ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
   126               (scan_lit ("</" ^ s) --| scan_whspc --| $$ ">"))) >>