src/Pure/System/isabelle_system.scala

 package isabelle
 
 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
 
 import scala.io.Source

   /* path specifications */
 
   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 =
   {
     val path = raw_path.expand
     require(path.is_absolute)

   }
 
 
   /* source files */
 
-  private def try_file(file: File) = if (file.isFile) Some(file) else None
-
-  def source_file(path: Path): Option[File] =
+  private def try_file(file: JFile) = if (file.isFile) Some(file) else None
+
+  def source_file(path: Path): Option[JFile] =
   {
     if (path.is_absolute || path.is_current)
       try_file(platform_file(path))
     else {
       val pure_file = (Path.explode("~~/src/Pure") + path).file

 
   /** external processes **/
 
   /* 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
       else args
     val env1 = if (env == null) settings else settings ++ env

     execute_env(null, null, redirect, args: _*)
 
 
   /* 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")
     private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
 

   }
 
 
   /* 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)
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
 

     }
   }
 
   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) }
 
     def terminate: Unit = thread.interrupt
     def is_finished: Boolean = result.is_finished