1.1 --- a/src/Pure/General/file.scala	Mon Jul 30 17:37:34 2012 +0200
     1.2 +++ b/src/Pure/General/file.scala	Mon Jul 30 20:43:07 2012 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  
     1.6  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
     1.7 -  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
     1.8 +  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile}
     1.9  import java.util.zip.GZIPOutputStream
    1.10  
    1.11  import scala.collection.mutable
    1.12 @@ -16,6 +16,23 @@
    1.13  
    1.14  object File
    1.15  {
    1.16 +  /* directory content */
    1.17 +
    1.18 +  def read_dir(dir: Path): List[String] =
    1.19 +  {
    1.20 +    if (!dir.is_dir) error("Bad directory: " + dir.toString)
    1.21 +    val files = dir.file.listFiles
    1.22 +    if (files == null) Nil
    1.23 +    else files.toList.map(_.getName)
    1.24 +  }
    1.25 +
    1.26 +  def find_files(dir: Path): Stream[Path] =
    1.27 +    read_dir(dir).toStream.map(name => {
    1.28 +      val path = dir + Path.basic(name)
    1.29 +      path #:: (if (path.is_dir) find_files(path) else Stream.empty)
    1.30 +    }).flatten
    1.31 +
    1.32 +
    1.33    /* read */
    1.34  
    1.35    def read(reader: BufferedReader): String =
    1.36 @@ -94,7 +111,7 @@
    1.37    def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
    1.38  
    1.39  
    1.40 -  /* misc */
    1.41 +  /* tmp files */
    1.42  
    1.43    def tmp_file(prefix: String): JFile =
    1.44    {
    1.45 @@ -108,19 +125,5 @@
    1.46      val file = tmp_file(prefix)
    1.47      try { body(file) } finally { file.delete }
    1.48    }
    1.49 -
    1.50 -  // FIXME handle (potentially cyclic) directory graph
    1.51 -  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
    1.52 -  {
    1.53 -    val files = new mutable.ListBuffer[JFile]
    1.54 -    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
    1.55 -    def find_entry(entry: JFile)
    1.56 -    {
    1.57 -      if (ok(entry)) files += entry
    1.58 -      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
    1.59 -    }
    1.60 -    find_entry(start)
    1.61 -    files.toList
    1.62 -  }
    1.63  }
    1.64  

     2.1 --- a/src/Tools/jEdit/src/scala_console.scala	Mon Jul 30 17:37:34 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Mon Jul 30 20:43:07 2012 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  import org.gjt.sp.jedit.MiscUtilities
     2.5  
     2.6  import java.lang.System
     2.7 -import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
     2.8 +import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
     2.9  
    2.10  import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    2.11  import scala.tools.nsc.interpreter.IMain
    2.12 @@ -28,9 +28,22 @@
    2.13  
    2.14    private def reconstruct_classpath(): String =
    2.15    {
    2.16 +    def find_files(start: JFile, ok: JFile => Boolean = _ => true): List[JFile] =
    2.17 +    {
    2.18 +      val files = new mutable.ListBuffer[JFile]
    2.19 +      val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
    2.20 +      def find_entry(entry: JFile)
    2.21 +      {
    2.22 +        if (ok(entry)) files += entry
    2.23 +        if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
    2.24 +      }
    2.25 +      find_entry(start)
    2.26 +      files.toList
    2.27 +    }
    2.28 +
    2.29      def find_jars(start: String): List[String] =
    2.30        if (start != null)
    2.31 -        File.find_files(new JFile(start),
    2.32 +        find_files(new JFile(start),
    2.33            entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    2.34        else Nil
    2.35      val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)