1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/General/file.scala Fri Jul 20 23:38:15 2012 +0200
1.3 @@ -0,0 +1,107 @@
1.4 +/* Title: Pure/General/file.scala
1.5 + Author: Makarius
1.6 +
1.7 +File system operations.
1.8 +*/
1.9 +
1.10 +package isabelle
1.11 +
1.12 +
1.13 +import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
1.14 + InputStream, FileInputStream, BufferedReader, InputStreamReader, File => JFile, FileFilter}
1.15 +import java.util.zip.GZIPOutputStream
1.16 +
1.17 +import scala.collection.mutable
1.18 +
1.19 +
1.20 +object File
1.21 +{
1.22 + /* read */
1.23 +
1.24 + def read(reader: BufferedReader): String =
1.25 + {
1.26 + val output = new StringBuilder(100)
1.27 + var c = -1
1.28 + while ({ c = reader.read; c != -1 }) output += c.toChar
1.29 + reader.close
1.30 + output.toString
1.31 + }
1.32 +
1.33 + def read(stream: InputStream): String =
1.34 + read(new BufferedReader(new InputStreamReader(stream, Standard_System.charset)))
1.35 +
1.36 + def read(file: JFile): String = read(new FileInputStream(file))
1.37 +
1.38 + def read(path: Path): String = read(path.file)
1.39 +
1.40 +
1.41 + /* write */
1.42 +
1.43 + private def write_file(file: JFile, text: CharSequence, zip: Boolean)
1.44 + {
1.45 + val stream1 = new FileOutputStream(file)
1.46 + val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
1.47 + val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset))
1.48 + try { writer.append(text) }
1.49 + finally { writer.close }
1.50 + }
1.51 +
1.52 + def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
1.53 + def write(path: Path, text: CharSequence): Unit = write(path.file, text)
1.54 +
1.55 + def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
1.56 + def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text)
1.57 +
1.58 +
1.59 + /* copy */
1.60 +
1.61 + def eq(file1: JFile, file2: JFile): Boolean =
1.62 + file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
1.63 +
1.64 + def copy(src: JFile, dst: JFile)
1.65 + {
1.66 + if (!eq(src, dst)) {
1.67 + val in = new FileInputStream(src)
1.68 + try {
1.69 + val out = new FileOutputStream(dst)
1.70 + try {
1.71 + val buf = new Array[Byte](65536)
1.72 + var m = 0
1.73 + do {
1.74 + m = in.read(buf, 0, buf.length)
1.75 + if (m != -1) out.write(buf, 0, m)
1.76 + } while (m != -1)
1.77 + }
1.78 + finally { out.close }
1.79 + }
1.80 + finally { in.close }
1.81 + }
1.82 + }
1.83 +
1.84 + def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
1.85 +
1.86 +
1.87 + /* misc */
1.88 +
1.89 + def with_tmp_file[A](prefix: String)(body: JFile => A): A =
1.90 + {
1.91 + val file = JFile.createTempFile(prefix, null)
1.92 + file.deleteOnExit
1.93 + try { body(file) } finally { file.delete }
1.94 + }
1.95 +
1.96 + // FIXME handle (potentially cyclic) directory graph
1.97 + def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
1.98 + {
1.99 + val files = new mutable.ListBuffer[JFile]
1.100 + val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
1.101 + def find_entry(entry: JFile)
1.102 + {
1.103 + if (ok(entry)) files += entry
1.104 + if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
1.105 + }
1.106 + find_entry(start)
1.107 + files.toList
1.108 + }
1.109 +}
1.110 +
2.1 --- a/src/Pure/General/path.scala Fri Jul 20 22:43:51 2012 +0200
2.2 +++ b/src/Pure/General/path.scala Fri Jul 20 23:38:15 2012 +0200
2.3 @@ -8,7 +8,7 @@
2.4 package isabelle
2.5
2.6
2.7 -import java.io.File
2.8 +import java.io.{File => JFile}
2.9
2.10 import scala.util.matching.Regex
2.11
2.12 @@ -168,5 +168,5 @@
2.13
2.14 /* platform file */
2.15
2.16 - def file: File = Isabelle_System.platform_file(this)
2.17 + def file: JFile = Isabelle_System.platform_file(this)
2.18 }
3.1 --- a/src/Pure/General/position.scala Fri Jul 20 22:43:51 2012 +0200
3.2 +++ b/src/Pure/General/position.scala Fri Jul 20 23:38:15 2012 +0200
3.3 @@ -7,6 +7,9 @@
3.4 package isabelle
3.5
3.6
3.7 +import java.io.{File => JFile}
3.8 +
3.9 +
3.10 object Position
3.11 {
3.12 type T = Properties.T
3.13 @@ -17,8 +20,8 @@
3.14 val File = new Properties.String(Isabelle_Markup.FILE)
3.15 val Id = new Properties.Long(Isabelle_Markup.ID)
3.16
3.17 - def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
3.18 - def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
3.19 + def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString))
3.20 + def line_file(i: Int, f: JFile): T = Line(i) ::: file(f)
3.21
3.22 object Range
3.23 {
4.1 --- a/src/Pure/General/scan.scala Fri Jul 20 22:43:51 2012 +0200
4.2 +++ b/src/Pure/General/scan.scala Fri Jul 20 23:38:15 2012 +0200
4.3 @@ -12,7 +12,7 @@
4.4 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
4.5 import scala.util.parsing.combinator.RegexParsers
4.6
4.7 -import java.io.{File, BufferedInputStream, FileInputStream}
4.8 +import java.io.{File => JFile, BufferedInputStream, FileInputStream}
4.9
4.10
4.11 object Scan
4.12 @@ -422,7 +422,7 @@
4.13
4.14 abstract class Byte_Reader extends Reader[Char] { def close: Unit }
4.15
4.16 - def byte_reader(file: File): Byte_Reader =
4.17 + def byte_reader(file: JFile): Byte_Reader =
4.18 {
4.19 val stream = new BufferedInputStream(new FileInputStream(file))
4.20 val seq = new PagedSeq(
5.1 --- a/src/Pure/General/sha1.scala Fri Jul 20 22:43:51 2012 +0200
5.2 +++ b/src/Pure/General/sha1.scala Fri Jul 20 23:38:15 2012 +0200
5.3 @@ -8,7 +8,7 @@
5.4 package isabelle
5.5
5.6
5.7 -import java.io.{File, FileInputStream}
5.8 +import java.io.{File => JFile, FileInputStream}
5.9 import java.security.MessageDigest
5.10
5.11
5.12 @@ -30,7 +30,7 @@
5.13 Digest(result.toString)
5.14 }
5.15
5.16 - def digest(file: File): Digest =
5.17 + def digest(file: JFile): Digest =
5.18 {
5.19 val stream = new FileInputStream(file)
5.20 val digest = MessageDigest.getInstance("SHA")
6.1 --- a/src/Pure/System/build.scala Fri Jul 20 22:43:51 2012 +0200
6.2 +++ b/src/Pure/System/build.scala Fri Jul 20 23:38:15 2012 +0200
6.3 @@ -7,7 +7,7 @@
6.4 package isabelle
6.5
6.6
6.7 -import java.io.File
6.8 +import java.io.{File => JFile}
6.9
6.10 import scala.collection.mutable
6.11 import scala.annotation.tailrec
6.12 @@ -140,9 +140,9 @@
6.13 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
6.14 }
6.15
6.16 - def parse_entries(root: File): List[Session_Entry] =
6.17 + def parse_entries(root: JFile): List[Session_Entry] =
6.18 {
6.19 - val toks = syntax.scan(Standard_System.read_file(root))
6.20 + val toks = syntax.scan(File.read(root))
6.21 parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
6.22 case Success(result, _) => result
6.23 case bad => error(bad.toString)
6.24 @@ -158,7 +158,7 @@
6.25
6.26 private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
6.27
6.28 - private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
6.29 + private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
6.30 {
6.31 (queue /: Parser.parse_entries(root))((queue1, entry) =>
6.32 try {
6.33 @@ -204,11 +204,10 @@
6.34 else queue
6.35 }
6.36
6.37 - private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
6.38 + private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
6.39 {
6.40 val dirs =
6.41 - split_lines(Standard_System.read_file(catalog)).
6.42 - filterNot(line => line == "" || line.startsWith("#"))
6.43 + split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
6.44 (queue /: dirs)((queue1, dir1) =>
6.45 try {
6.46 val dir2 = dir + Path.explode(dir1)
6.47 @@ -275,15 +274,12 @@
6.48 !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
6.49 {
6.50 Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
6.51 - Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
6.52 - Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
6.53 - Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
6.54 - Standard_System.read_file(
6.55 - Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
6.56 - Standard_System.read_file(
6.57 - Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
6.58 - Standard_System.read_file(
6.59 - Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
6.60 + File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
6.61 + Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
6.62 + File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
6.63 + File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
6.64 + File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
6.65 + File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
6.66 }
6.67
6.68 // prepare log dir
6.69 @@ -304,10 +300,10 @@
6.70
6.71 val log = log_dir + Path.basic(key.name)
6.72 if (rc == 0) {
6.73 - Standard_System.write_file(log.ext("gz").file, out, true)
6.74 + File.write_zip(log.ext("gz"), out)
6.75 }
6.76 else {
6.77 - Standard_System.write_file(log.file, out)
6.78 + File.write(log, out)
6.79 echo(key.name + " FAILED")
6.80 echo("(see also " + log.file + ")")
6.81 val lines = split_lines(out)
7.1 --- a/src/Pure/System/isabelle_system.scala Fri Jul 20 22:43:51 2012 +0200
7.2 +++ b/src/Pure/System/isabelle_system.scala Fri Jul 20 23:38:15 2012 +0200
7.3 @@ -10,7 +10,7 @@
7.4 import java.lang.System
7.5 import java.util.regex.Pattern
7.6 import java.util.Locale
7.7 -import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
7.8 +import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
7.9 BufferedWriter, OutputStreamWriter, IOException}
7.10 import java.awt.{GraphicsEnvironment, Font}
7.11 import java.awt.font.TextAttribute
7.12 @@ -68,7 +68,7 @@
7.13 case Some(path) => path
7.14 }
7.15
7.16 - Standard_System.with_tmp_file("settings") { dump =>
7.17 + File.with_tmp_file("settings") { dump =>
7.18 val shell_prefix =
7.19 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
7.20 else Nil
7.21 @@ -78,7 +78,7 @@
7.22 if (rc != 0) error(output)
7.23
7.24 val entries =
7.25 - (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {
7.26 + (for (entry <- File.read(dump) split "\0" if entry != "") yield {
7.27 val i = entry.indexOf('=')
7.28 if (i <= 0) (entry -> "")
7.29 else (entry.substring(0, i) -> entry.substring(i + 1))
7.30 @@ -109,7 +109,7 @@
7.31 def standard_path(path: Path): String = path.expand.implode
7.32
7.33 def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
7.34 - def platform_file(path: Path): File = new File(platform_path(path))
7.35 + def platform_file(path: Path): JFile = new JFile(platform_path(path))
7.36
7.37 def platform_file_url(raw_path: Path): String =
7.38 {
7.39 @@ -132,16 +132,16 @@
7.40 for {
7.41 path <- paths
7.42 file = platform_file(path) if file.isFile
7.43 - } { buf.append(Standard_System.read_file(file)); buf.append('\n') }
7.44 + } { buf.append(File.read(file)); buf.append('\n') }
7.45 buf.toString
7.46 }
7.47
7.48
7.49 /* source files */
7.50
7.51 - private def try_file(file: File) = if (file.isFile) Some(file) else None
7.52 + private def try_file(file: JFile) = if (file.isFile) Some(file) else None
7.53
7.54 - def source_file(path: Path): Option[File] =
7.55 + def source_file(path: Path): Option[JFile] =
7.56 {
7.57 if (path.is_absolute || path.is_current)
7.58 try_file(platform_file(path))
7.59 @@ -159,7 +159,7 @@
7.60
7.61 /* plain execute */
7.62
7.63 - def execute_env(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
7.64 + def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
7.65 {
7.66 val cmdline =
7.67 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
7.68 @@ -174,7 +174,7 @@
7.69
7.70 /* managed process */
7.71
7.72 - class Managed_Process(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
7.73 + class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
7.74 {
7.75 private val params =
7.76 List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
7.77 @@ -241,15 +241,15 @@
7.78
7.79 /* bash */
7.80
7.81 - def bash_env(cwd: File, env: Map[String, String], script: String): (String, String, Int) =
7.82 + def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
7.83 {
7.84 - Standard_System.with_tmp_file("isabelle_script") { script_file =>
7.85 - Standard_System.write_file(script_file, script)
7.86 + File.with_tmp_file("isabelle_script") { script_file =>
7.87 + File.write(script_file, script)
7.88 val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
7.89
7.90 proc.stdin.close
7.91 - val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
7.92 - val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
7.93 + val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
7.94 + val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
7.95
7.96 val rc =
7.97 try { proc.join }
7.98 @@ -260,7 +260,7 @@
7.99
7.100 def bash(script: String): (String, String, Int) = bash_env(null, null, script)
7.101
7.102 - class Bash_Job(cwd: File, env: Map[String, String], script: String)
7.103 + class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
7.104 {
7.105 private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
7.106
8.1 --- a/src/Pure/System/options.scala Fri Jul 20 22:43:51 2012 +0200
8.2 +++ b/src/Pure/System/options.scala Fri Jul 20 23:38:15 2012 +0200
8.3 @@ -7,7 +7,7 @@
8.4 package isabelle
8.5
8.6
8.7 -import java.io.File
8.8 +import java.io.{File => JFile}
8.9
8.10
8.11 object Options
8.12 @@ -49,10 +49,9 @@
8.13 { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
8.14 }
8.15
8.16 - def parse_entries(file: File): List[Options => Options] =
8.17 + def parse_entries(file: JFile): List[Options => Options] =
8.18 {
8.19 - val toks = syntax.scan(Standard_System.read_file(file))
8.20 - parse_all(rep(entry), Token.reader(toks, file.toString)) match {
8.21 + parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
8.22 case Success(result, _) => result
8.23 case bad => error(bad.toString)
8.24 }
9.1 --- a/src/Pure/System/session_manager.scala Fri Jul 20 22:43:51 2012 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,48 +0,0 @@
9.4 -/* Title: Pure/System/isabelle_manager.scala
9.5 - Author: Makarius
9.6 -
9.7 -Isabelle session manager.
9.8 -*/
9.9 -
9.10 -package isabelle
9.11 -
9.12 -
9.13 -import java.io.{File, FileFilter}
9.14 -
9.15 -
9.16 -class Session_Manager
9.17 -{
9.18 - val ROOT_NAME = "session.root"
9.19 -
9.20 - def is_session_file(file: File): Boolean =
9.21 - file.isFile && file.getName == ROOT_NAME
9.22 -
9.23 - def is_session_dir(dir: File): Boolean =
9.24 - dir.isDirectory && (new File(dir, ROOT_NAME)).isFile
9.25 -
9.26 -
9.27 - // FIXME handle (potentially cyclic) directory graph
9.28 - private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
9.29 - dir: File): List[List[String]] =
9.30 - {
9.31 - val (reverse_prefix1, reverse_sessions1) =
9.32 - if (is_session_dir(dir)) {
9.33 - val name = dir.getName // FIXME from root file
9.34 - val reverse_prefix1 = name :: reverse_prefix
9.35 - val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
9.36 - (reverse_prefix1, reverse_sessions1)
9.37 - }
9.38 - else (reverse_prefix, reverse_sessions)
9.39 -
9.40 - val subdirs =
9.41 - dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
9.42 - (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
9.43 - }
9.44 -
9.45 - def component_sessions(): List[List[String]] =
9.46 - {
9.47 - val toplevel_sessions =
9.48 - Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir)
9.49 - ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
9.50 - }
9.51 -}
10.1 --- a/src/Pure/System/standard_system.scala Fri Jul 20 22:43:51 2012 +0200
10.2 +++ b/src/Pure/System/standard_system.scala Fri Jul 20 23:38:15 2012 +0200
10.3 @@ -11,15 +11,11 @@
10.4 import java.util.regex.Pattern
10.5 import java.util.Locale
10.6 import java.net.URL
10.7 -import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
10.8 - BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
10.9 - File, FileFilter, IOException}
10.10 +import java.io.{File => JFile}
10.11 import java.nio.charset.Charset
10.12 -import java.util.zip.GZIPOutputStream
10.13
10.14 import scala.io.Codec
10.15 import scala.util.matching.Regex
10.16 -import scala.collection.mutable
10.17
10.18
10.19 object Standard_System
10.20 @@ -100,77 +96,9 @@
10.21 }
10.22
10.23
10.24 - /* basic file operations */
10.25 -
10.26 - def slurp(reader: BufferedReader): String =
10.27 - {
10.28 - val output = new StringBuilder(100)
10.29 - var c = -1
10.30 - while ({ c = reader.read; c != -1 }) output += c.toChar
10.31 - reader.close
10.32 - output.toString
10.33 - }
10.34 -
10.35 - def slurp(stream: InputStream): String =
10.36 - slurp(new BufferedReader(new InputStreamReader(stream, charset)))
10.37 -
10.38 - def read_file(file: File): String = slurp(new FileInputStream(file))
10.39 -
10.40 - def write_file(file: File, text: CharSequence, zip: Boolean = false)
10.41 - {
10.42 - val stream1 = new FileOutputStream(file)
10.43 - val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
10.44 - val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
10.45 - try { writer.append(text) }
10.46 - finally { writer.close }
10.47 - }
10.48 -
10.49 - def eq_file(file1: File, file2: File): Boolean =
10.50 - file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
10.51 -
10.52 - def copy_file(src: File, dst: File) =
10.53 - if (!eq_file(src, dst)) {
10.54 - val in = new FileInputStream(src)
10.55 - try {
10.56 - val out = new FileOutputStream(dst)
10.57 - try {
10.58 - val buf = new Array[Byte](65536)
10.59 - var m = 0
10.60 - do {
10.61 - m = in.read(buf, 0, buf.length)
10.62 - if (m != -1) out.write(buf, 0, m)
10.63 - } while (m != -1)
10.64 - }
10.65 - finally { out.close }
10.66 - }
10.67 - finally { in.close }
10.68 - }
10.69 -
10.70 - def with_tmp_file[A](prefix: String)(body: File => A): A =
10.71 - {
10.72 - val file = File.createTempFile(prefix, null)
10.73 - file.deleteOnExit
10.74 - try { body(file) } finally { file.delete }
10.75 - }
10.76 -
10.77 - // FIXME handle (potentially cyclic) directory graph
10.78 - def find_files(start: File, ok: File => Boolean): List[File] =
10.79 - {
10.80 - val files = new mutable.ListBuffer[File]
10.81 - val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
10.82 - def find_entry(entry: File)
10.83 - {
10.84 - if (ok(entry)) files += entry
10.85 - if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
10.86 - }
10.87 - find_entry(start)
10.88 - files.toList
10.89 - }
10.90 -
10.91 -
10.92 /* shell processes */
10.93
10.94 - def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
10.95 + def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
10.96 {
10.97 val cmdline = new java.util.LinkedList[String]
10.98 for (s <- args) cmdline.add(s)
10.99 @@ -188,7 +116,7 @@
10.100 def process_output(proc: Process): (String, Int) =
10.101 {
10.102 proc.getOutputStream.close
10.103 - val output = slurp(proc.getInputStream)
10.104 + val output = File.read(proc.getInputStream)
10.105 val rc =
10.106 try { proc.waitFor }
10.107 finally {
10.108 @@ -200,7 +128,7 @@
10.109 (output, rc)
10.110 }
10.111
10.112 - def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
10.113 + def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
10.114 : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
10.115
10.116
10.117 @@ -215,10 +143,10 @@
10.118 else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
10.119 else error("Bad Cygwin installation: unknown root")
10.120
10.121 - val root_file = new File(root)
10.122 - if (!new File(root_file, "bin\\bash.exe").isFile ||
10.123 - !new File(root_file, "bin\\env.exe").isFile ||
10.124 - !new File(root_file, "bin\\tar.exe").isFile)
10.125 + val root_file = new JFile(root)
10.126 + if (!new JFile(root_file, "bin\\bash.exe").isFile ||
10.127 + !new JFile(root_file, "bin\\env.exe").isFile ||
10.128 + !new JFile(root_file, "bin\\tar.exe").isFile)
10.129 error("Bad Cygwin installation: " + quote(root))
10.130
10.131 root
10.132 @@ -244,11 +172,11 @@
10.133 val rest =
10.134 posix_path match {
10.135 case Cygdrive(drive, rest) =>
10.136 - result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + File.separator)
10.137 + result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
10.138 rest
10.139 case Named_Root(root, rest) =>
10.140 - result_path ++= File.separator
10.141 - result_path ++= File.separator
10.142 + result_path ++= JFile.separator
10.143 + result_path ++= JFile.separator
10.144 result_path ++= root
10.145 rest
10.146 case path if path.startsWith("/") =>
10.147 @@ -258,8 +186,8 @@
10.148 }
10.149 for (p <- space_explode('/', rest) if p != "") {
10.150 val len = result_path.length
10.151 - if (len > 0 && result_path(len - 1) != File.separatorChar)
10.152 - result_path += File.separatorChar
10.153 + if (len > 0 && result_path(len - 1) != JFile.separatorChar)
10.154 + result_path += JFile.separatorChar
10.155 result_path ++= p
10.156 }
10.157 result_path.toString
10.158 @@ -292,11 +220,11 @@
10.159 def this_jdk_home(): String =
10.160 {
10.161 val java_home = System.getProperty("java.home")
10.162 - val home = new File(java_home)
10.163 + val home = new JFile(java_home)
10.164 val parent = home.getParent
10.165 val jdk_home =
10.166 if (home.getName == "jre" && parent != null &&
10.167 - (new File(new File(parent, "bin"), "javac")).exists) parent
10.168 + (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
10.169 else java_home
10.170 posix_path(jdk_home)
10.171 }
11.1 --- a/src/Pure/System/system_channel.scala Fri Jul 20 22:43:51 2012 +0200
11.2 +++ b/src/Pure/System/system_channel.scala Fri Jul 20 23:38:15 2012 +0200
11.3 @@ -8,7 +8,8 @@
11.4 package isabelle
11.5
11.6
11.7 -import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
11.8 +import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
11.9 + FileOutputStream, IOException}
11.10 import java.net.{ServerSocket, InetAddress}
11.11
11.12
12.1 --- a/src/Pure/Thy/thy_header.scala Fri Jul 20 22:43:51 2012 +0200
12.2 +++ b/src/Pure/Thy/thy_header.scala Fri Jul 20 23:38:15 2012 +0200
12.3 @@ -12,7 +12,7 @@
12.4 import scala.util.parsing.input.{Reader, CharSequenceReader}
12.5 import scala.util.matching.Regex
12.6
12.7 -import java.io.File
12.8 +import java.io.{File => JFile}
12.9
12.10
12.11 object Thy_Header extends Parse.Parser
12.12 @@ -102,7 +102,7 @@
12.13 def read(source: CharSequence): Thy_Header =
12.14 read(new CharSequenceReader(source))
12.15
12.16 - def read(file: File): Thy_Header =
12.17 + def read(file: JFile): Thy_Header =
12.18 {
12.19 val reader = Scan.byte_reader(file)
12.20 try { read(reader).map(Standard_System.decode_permissive_utf8) }
13.1 --- a/src/Pure/Thy/thy_load.scala Fri Jul 20 22:43:51 2012 +0200
13.2 +++ b/src/Pure/Thy/thy_load.scala Fri Jul 20 23:38:15 2012 +0200
13.3 @@ -7,7 +7,7 @@
13.4 package isabelle
13.5
13.6
13.7 -import java.io.File
13.8 +import java.io.{File => JFile}
13.9
13.10
13.11
13.12 @@ -31,7 +31,7 @@
13.13
13.14 def read_header(name: Document.Node.Name): Thy_Header =
13.15 {
13.16 - val file = new File(name.node)
13.17 + val file = new JFile(name.node)
13.18 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
13.19 Thy_Header.read(file)
13.20 }
14.1 --- a/src/Pure/build-jars Fri Jul 20 22:43:51 2012 +0200
14.2 +++ b/src/Pure/build-jars Fri Jul 20 23:38:15 2012 +0200
14.3 @@ -14,6 +14,7 @@
14.4 Concurrent/simple_thread.scala
14.5 Concurrent/volatile.scala
14.6 General/exn.scala
14.7 + General/file.scala
14.8 General/graph.scala
14.9 General/linear_set.scala
14.10 General/path.scala
14.11 @@ -51,7 +52,6 @@
14.12 System/options.scala
14.13 System/platform.scala
14.14 System/session.scala
14.15 - System/session_manager.scala
14.16 System/standard_system.scala
14.17 System/swing_thread.scala
14.18 System/system_channel.scala
15.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Fri Jul 20 22:43:51 2012 +0200
15.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Fri Jul 20 23:38:15 2012 +0200
15.3 @@ -9,7 +9,7 @@
15.4
15.5 import isabelle._
15.6
15.7 -import java.io.File
15.8 +import java.io.{File => JFile}
15.9
15.10 import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
15.11
16.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala Fri Jul 20 22:43:51 2012 +0200
16.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala Fri Jul 20 23:38:15 2012 +0200
16.3 @@ -9,7 +9,7 @@
16.4
16.5 import isabelle._
16.6
16.7 -import java.io.{File, IOException}
16.8 +import java.io.{File => JFile, IOException}
16.9 import javax.swing.text.Segment
16.10
16.11 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
16.12 @@ -65,7 +65,7 @@
16.13 case None => None
16.14 }
16.15 } getOrElse {
16.16 - val file = new File(name.node) // FIXME load URL via jEdit VFS (!?)
16.17 + val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?)
16.18 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
16.19 Thy_Header.read(file)
16.20 }
17.1 --- a/src/Tools/jEdit/src/scala_console.scala Fri Jul 20 22:43:51 2012 +0200
17.2 +++ b/src/Tools/jEdit/src/scala_console.scala Fri Jul 20 23:38:15 2012 +0200
17.3 @@ -15,7 +15,7 @@
17.4 import org.gjt.sp.jedit.MiscUtilities
17.5
17.6 import java.lang.System
17.7 -import java.io.{File, OutputStream, Writer, PrintWriter}
17.8 +import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
17.9
17.10 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
17.11 import scala.tools.nsc.interpreter.IMain
17.12 @@ -30,11 +30,11 @@
17.13 {
17.14 def find_jars(start: String): List[String] =
17.15 if (start != null)
17.16 - Standard_System.find_files(new File(start),
17.17 + File.find_files(new JFile(start),
17.18 entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
17.19 else Nil
17.20 val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
17.21 - path.mkString(File.pathSeparator)
17.22 + path.mkString(JFile.pathSeparator)
17.23 }
17.24
17.25