clarified directory content operations (similar to ML version);

--- a/src/Pure/General/file.scala	Mon Jul 30 17:37:34 2012 +0200
+++ b/src/Pure/General/file.scala	Mon Jul 30 20:43:07 2012 +0200
@@ -8,7 +8,7 @@
 
 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
-  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
+  InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile}
 import java.util.zip.GZIPOutputStream
 
 import scala.collection.mutable
@@ -16,6 +16,23 @@
 
 object File
 {
+  /* directory content */
+
+  def read_dir(dir: Path): List[String] =
+  {
+    if (!dir.is_dir) error("Bad directory: " + dir.toString)
+    val files = dir.file.listFiles
+    if (files == null) Nil
+    else files.toList.map(_.getName)
+  }
+
+  def find_files(dir: Path): Stream[Path] =
+    read_dir(dir).toStream.map(name => {
+      val path = dir + Path.basic(name)
+      path #:: (if (path.is_dir) find_files(path) else Stream.empty)
+    }).flatten
+
+
   /* read */
 
   def read(reader: BufferedReader): String =
@@ -94,7 +111,7 @@
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
 
 
-  /* misc */
+  /* tmp files */
 
   def tmp_file(prefix: String): JFile =
   {
@@ -108,19 +125,5 @@
     val file = tmp_file(prefix)
     try { body(file) } finally { file.delete }
   }
-
-  // FIXME handle (potentially cyclic) directory graph
-  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
-  {
-    val files = new mutable.ListBuffer[JFile]
-    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
-    def find_entry(entry: JFile)
-    {
-      if (ok(entry)) files += entry
-      if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
-    }
-    find_entry(start)
-    files.toList
-  }
 }
 

--- a/src/Tools/jEdit/src/scala_console.scala	Mon Jul 30 17:37:34 2012 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Mon Jul 30 20:43:07 2012 +0200
@@ -15,7 +15,7 @@
 import org.gjt.sp.jedit.MiscUtilities
 
 import java.lang.System
-import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
+import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
 import scala.tools.nsc.interpreter.IMain
@@ -28,9 +28,22 @@
 
   private def reconstruct_classpath(): String =
   {
+    def find_files(start: JFile, ok: JFile => Boolean = _ => true): List[JFile] =
+    {
+      val files = new mutable.ListBuffer[JFile]
+      val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
+      def find_entry(entry: JFile)
+      {
+        if (ok(entry)) files += entry
+        if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
+      }
+      find_entry(start)
+      files.toList
+    }
+
     def find_jars(start: String): List[String] =
       if (start != null)
-        File.find_files(new JFile(start),
+        find_files(new JFile(start),
           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
       else Nil
     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)