# HG changeset patch
# User aspinall
# Date 1096490440 -7200
# Node ID 2fac1f11b7f6b667ada4f55b6f674d6b7d94d235
# Parent  6bd87812537c6671531db2d4bf2dfccb8edd3673
Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.

diff -r 6bd87812537c -r 2fac1f11b7f6 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Wed Sep 29 18:32:25 2004 +0200
+++ b/src/Pure/General/xml.ML	Wed Sep 29 22:40:40 2004 +0200
@@ -103,7 +103,7 @@
 
 val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
 
-val parse_chars = Scan.repeat1 (Scan.unless (scan_whspc -- $$ "<")
+val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
   (scan_special || Scan.one Symbol.not_eof)) >> implode;
 
 val parse_cdata = Scan.this_string "<![CDATA[" |--
@@ -127,14 +127,14 @@
   Scan.this_string "?>";
 
 fun parse_content xs =
-  ((Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) [] --
-    (Scan.repeat (scan_whspc |--
+  ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
+    (Scan.repeat ((* scan_whspc |-- *)
        (   parse_elem >> single
         || parse_cdata >> (single o Text)
         || parse_pi >> K []
         || parse_comment >> K []) --
-       Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) []
-         >> op @) >> flat) >> op @) --| scan_whspc) xs
+       Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
+         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
 
 and parse_elem xs =
   ($$ "<" |-- Symbol.scan_id --