Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
authoraspinall
Wed Sep 29 22:40:40 2004 +0200 (2004-09-29)
changeset 152162fac1f11b7f6
parent 15215 6bd87812537c
child 15217 15fa818ef624
Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
src/Pure/General/xml.ML
     1.1 --- a/src/Pure/General/xml.ML	Wed Sep 29 18:32:25 2004 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Wed Sep 29 22:40:40 2004 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
     1.6  
     1.7 -val parse_chars = Scan.repeat1 (Scan.unless (scan_whspc -- $$ "<")
     1.8 +val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
     1.9    (scan_special || Scan.one Symbol.not_eof)) >> implode;
    1.10  
    1.11  val parse_cdata = Scan.this_string "<![CDATA[" |--
    1.12 @@ -127,14 +127,14 @@
    1.13    Scan.this_string "?>";
    1.14  
    1.15  fun parse_content xs =
    1.16 -  ((Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) [] --
    1.17 -    (Scan.repeat (scan_whspc |--
    1.18 +  ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
    1.19 +    (Scan.repeat ((* scan_whspc |-- *)
    1.20         (   parse_elem >> single
    1.21          || parse_cdata >> (single o Text)
    1.22          || parse_pi >> K []
    1.23          || parse_comment >> K []) --
    1.24 -       Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) []
    1.25 -         >> op @) >> flat) >> op @) --| scan_whspc) xs
    1.26 +       Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
    1.27 +         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
    1.28  
    1.29  and parse_elem xs =
    1.30    ($$ "<" |-- Symbol.scan_id --