# HG changeset patch
# User wenzelm
# Date 1310834495 -7200
# Node ID 8f2bf02a0ccbde39b79271ba0443aa986dbe8a73
# Parent  529159f81d06d8c053e10a87c5d50eec216541cc
some file and directory operations;

diff -r 529159f81d06 -r 8f2bf02a0ccb src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Jul 16 18:20:02 2011 +0200
+++ b/src/Pure/General/file.ML	Sat Jul 16 18:41:35 2011 +0200
@@ -18,11 +18,15 @@
   val is_dir: Path.T -> bool
   val check_dir: Path.T -> Path.T
   val check_file: Path.T -> Path.T
+  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
+  val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val read_dir: Path.T -> string list
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val read_lines: Path.T -> string list
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
@@ -91,7 +95,7 @@
   else error ("No such file: " ^ Path.print path);
 
 
-(* open files *)
+(* open streams *)
 
 local
 
@@ -101,6 +105,7 @@
 
 in
 
+fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
 fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path;
 fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path;
 fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
@@ -108,6 +113,19 @@
 end;
 
 
+(* directory content *)
+
+fun fold_dir f path a = open_dir (fn stream =>
+  let
+    fun read x =
+      (case OS.FileSys.readDir stream of
+        NONE => x
+      | SOME entry => read (f entry x));
+  in read a end) path;
+
+fun read_dir path = rev (fold_dir cons path []);
+
+
 (* input *)
 
 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
@@ -127,6 +145,8 @@
 fun fold_lines f = fold_chunks #"\n" f;
 fun fold_pages f = fold_chunks #"\f" f;
 
+fun read_lines path = rev (fold_lines cons path []);
+
 val read = open_input TextIO.inputAll;