src/Pure/PIDE/xml.ML
changeset 61476 1884c40f1539
parent 60982 67e389f67073
child 61707 d5ddd022a451
--- a/src/Pure/PIDE/xml.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/PIDE/xml.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -239,12 +239,12 @@
 
 fun parse_content xs =
   (parse_optional_text @@@
-    (Scan.repeat
+    Scan.repeats
       ((parse_element >> single ||
         parse_cdata >> (single o Text) ||
         parse_processing_instruction ||
         parse_comment)
-      @@@ parse_optional_text) >> flat)) xs
+      @@@ parse_optional_text)) xs
 
 and parse_element xs =
   ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--