# HG changeset patch
# User noschinl
# Date 1302786282 -7200
# Node ID ce00462fe8aade9033a296b8ffba45528aa94a7d
# Parent  79309a48a4a7817245fc28d397ade6d154badb79
turn YXML.parse_file into a fold

diff -r 79309a48a4a7 -r ce00462fe8aa src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/Pure/General/yxml.ML	Thu Apr 14 15:04:42 2011 +0200
@@ -21,7 +21,7 @@
   val string_of: XML.tree -> string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
-  val parse_file: (XML.tree -> 'a) -> Path.T -> 'a list
+  val parse_file: (XML.tree -> 'a -> 'a) -> Path.T -> 'a -> 'a
 end;
 
 structure YXML: YXML =
@@ -124,8 +124,8 @@
 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));
+        [(("", _), [result])] => (stack_init, f result results)
+      | x => (x, results));
 
 in
 
@@ -140,10 +140,11 @@
   | [] => XML.Text ""
   | _ => err "multiple results");
 
-fun parse_file f path =
+(*folds a function over each XML.Tree in the file*)
+fun parse_file f path s =
   (case File.fold_fields (is_char X) (preparse_chunk f)
-      path  (stack_init, []) of
-    ([(("", _), [])], result) => rev result
+      path (stack_init, s) of
+    ([(("", _), [])], result) => result
   | (((name, _), _) :: _, _) => err_unbalanced name);
 
 end;