src/Pure/General/yxml.ML

   | push name atts pending = ((name, atts), []) :: pending;
 
 fun pop ((("", _), _) :: _) = err_unbalanced ""
   | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
 
+val stack_init = [(("", []), [])];
 
 (* parsing *)
 
 fun parse_attrib s =
   (case first_field "=" s of

 
 fun parse_chunk ["", ""] = pop
   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
   | parse_chunk txts = fold (add o XML.Text) txts;
 
+fun preparse_chunk _ "" x = x
+  | preparse_chunk f str (pending, results) =
+      (case parse_chunk (String.fields (is_char Y) str) pending of
+        [(("", _), [result])] => (stack_init, f result :: results)
+      | foo => (foo, results));
+
 in
 
 fun parse_body source =
-  (case fold parse_chunk (split_string source) [(("", []), [])] of
+  (case fold parse_chunk (split_string source) stack_init of
     [(("", _), result)] => rev result
   | ((name, _), _) :: _ => err_unbalanced name);
 
 fun parse source =
   (case parse_body source of
     [result] => result
   | [] => XML.Text ""
   | _ => err "multiple results");
 
+fun parse_file' f path =
+  (case File.fold_fields (is_char X) (preparse_chunk f)
+      path  (stack_init, []) of
+    ([(("", _), [])], result) => rev result
+  | (((name, _), _) :: _, _) => err_unbalanced name);
+
 end;
 
 end;