src/Pure/System/isabelle_system.scala

--- a/src/Pure/System/isabelle_system.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -10,7 +10,7 @@
 import java.lang.System
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
+import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
   BufferedWriter, OutputStreamWriter, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 import java.awt.font.TextAttribute
@@ -109,7 +109,7 @@
   def standard_path(path: Path): String = path.expand.implode
 
   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
-  def platform_file(path: Path): File = new File(platform_path(path))
+  def platform_file(path: Path): JFile = new JFile(platform_path(path))
 
   def platform_file_url(raw_path: Path): String =
   {
@@ -139,9 +139,9 @@
 
   /* source files */
 
-  private def try_file(file: File) = if (file.isFile) Some(file) else None
+  private def try_file(file: JFile) = if (file.isFile) Some(file) else None
 
-  def source_file(path: Path): Option[File] =
+  def source_file(path: Path): Option[JFile] =
   {
     if (path.is_absolute || path.is_current)
       try_file(platform_file(path))
@@ -159,7 +159,7 @@
 
   /* plain execute */
 
-  def execute_env(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
+  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline =
       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
@@ -174,7 +174,7 @@
 
   /* managed process */
 
-  class Managed_Process(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
+  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
   {
     private val params =
       List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
@@ -241,7 +241,7 @@
 
   /* bash */
 
-  def bash_env(cwd: File, env: Map[String, String], script: String): (String, String, Int) =
+  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
   {
     Standard_System.with_tmp_file("isabelle_script") { script_file =>
       Standard_System.write_file(script_file, script)
@@ -260,7 +260,7 @@
 
   def bash(script: String): (String, String, Int) = bash_env(null, null, script)
 
-  class Bash_Job(cwd: File, env: Map[String, String], script: String)
+  class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
   {
     private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }