# HG changeset patch
# User wenzelm
# Date 1263057782 -3600
# Node ID 13e9f1f4acd95abae7ec533a578055a412bac936
# Parent  5c0a2583f9977c418a0ca7e591aede8efe57d2e0
added find_files;

diff -r 5c0a2583f997 -r 13e9f1f4acd9 src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Sat Jan 09 18:22:40 2010 +0100
+++ b/src/Pure/System/standard_system.scala	Sat Jan 09 18:23:02 2010 +0100
@@ -10,7 +10,7 @@
 import java.util.Locale
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
   BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
-  File, IOException}
+  File, FileFilter, IOException}
 
 import scala.io.Source
 import scala.util.matching.Regex
@@ -98,6 +98,19 @@
     finally { writer.close }
   }
 
+  def find_files(start: File, ok: File => Boolean): List[File] =
+  {
+    val files = new mutable.ListBuffer[File]
+    val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
+    def find_entry(entry: File)
+    {
+      if (ok(entry)) files += entry
+      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
+    }
+    find_entry(start)
+    files.toList
+  }
+
 
   /* shell processes */