# HG changeset patch # User wenzelm # Date 1343673787 -7200 # Node ID 232652ac346e63f0f93cba06b661ccb71255f6e2 # Parent 795d38a6dab3409bf4702f1fbe6df62b3e9ae752 clarified directory content operations (similar to ML version); diff -r 795d38a6dab3 -r 232652ac346e src/Pure/General/file.scala --- 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 - } } diff -r 795d38a6dab3 -r 232652ac346e src/Tools/jEdit/src/scala_console.scala --- 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)