src/Pure/System/standard_system.scala
changeset 34298 13e9f1f4acd9
parent 34258 e936d3c35ce0
child 34300 3f2e25dc99ab
     1.1 --- a/src/Pure/System/standard_system.scala	Sat Jan 09 18:22:40 2010 +0100
     1.2 +++ b/src/Pure/System/standard_system.scala	Sat Jan 09 18:23:02 2010 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  import java.util.Locale
     1.5  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
     1.6    BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.7 -  File, IOException}
     1.8 +  File, FileFilter, IOException}
     1.9  
    1.10  import scala.io.Source
    1.11  import scala.util.matching.Regex
    1.12 @@ -98,6 +98,19 @@
    1.13      finally { writer.close }
    1.14    }
    1.15  
    1.16 +  def find_files(start: File, ok: File => Boolean): List[File] =
    1.17 +  {
    1.18 +    val files = new mutable.ListBuffer[File]
    1.19 +    val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
    1.20 +    def find_entry(entry: File)
    1.21 +    {
    1.22 +      if (ok(entry)) files += entry
    1.23 +      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
    1.24 +    }
    1.25 +    find_entry(start)
    1.26 +    files.toList
    1.27 +  }
    1.28 +
    1.29  
    1.30    /* shell processes */
    1.31