# HG changeset patch
# User noschinl
# Date 1302723480 -7200
# Node ID b3759dcea95e2181f29b2421302549aff2d2ab73
# Parent  7a1655920fe8f589061c3bb07b580f3167159a0f
Add YXML.parse_file to signature ...

diff -r 7a1655920fe8 -r b3759dcea95e src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Wed Apr 13 21:23:30 2011 +0200
+++ b/src/Pure/General/yxml.ML	Wed Apr 13 21:38:00 2011 +0200
@@ -21,6 +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
 end;
 
 structure YXML: YXML =
@@ -139,7 +140,7 @@
   | [] => XML.Text ""
   | _ => err "multiple results");
 
-fun parse_file' f path =
+fun parse_file f path =
   (case File.fold_fields (is_char X) (preparse_chunk f)
       path  (stack_init, []) of
     ([(("", _), [])], result) => rev result