1.1 --- a/src/Pure/General/path.scala	Fri Jul 20 21:05:47 2012 +0200
     1.2 +++ b/src/Pure/General/path.scala	Fri Jul 20 22:29:25 2012 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.io.File
     1.8 +import java.io.{File => JFile}
     1.9  
    1.10  import scala.util.matching.Regex
    1.11  
    1.12 @@ -168,5 +168,5 @@
    1.13  
    1.14    /* platform file */
    1.15  
    1.16 -  def file: File = Isabelle_System.platform_file(this)
    1.17 +  def file: JFile = Isabelle_System.platform_file(this)
    1.18  }

     2.1 --- a/src/Pure/General/position.scala	Fri Jul 20 21:05:47 2012 +0200
     2.2 +++ b/src/Pure/General/position.scala	Fri Jul 20 22:29:25 2012 +0200
     2.3 @@ -7,6 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +
     2.9 +
    2.10  object Position
    2.11  {
    2.12    type T = Properties.T
    2.13 @@ -17,8 +20,8 @@
    2.14    val File = new Properties.String(Isabelle_Markup.FILE)
    2.15    val Id = new Properties.Long(Isabelle_Markup.ID)
    2.16  
    2.17 -  def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
    2.18 -  def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
    2.19 +  def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString))
    2.20 +  def line_file(i: Int, f: JFile): T = Line(i) ::: file(f)
    2.21  
    2.22    object Range
    2.23    {

     3.1 --- a/src/Pure/General/scan.scala	Fri Jul 20 21:05:47 2012 +0200
     3.2 +++ b/src/Pure/General/scan.scala	Fri Jul 20 22:29:25 2012 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
     3.5  import scala.util.parsing.combinator.RegexParsers
     3.6  
     3.7 -import java.io.{File, BufferedInputStream, FileInputStream}
     3.8 +import java.io.{File => JFile, BufferedInputStream, FileInputStream}
     3.9  
    3.10  
    3.11  object Scan
    3.12 @@ -422,7 +422,7 @@
    3.13  
    3.14    abstract class Byte_Reader extends Reader[Char] { def close: Unit }
    3.15  
    3.16 -  def byte_reader(file: File): Byte_Reader =
    3.17 +  def byte_reader(file: JFile): Byte_Reader =
    3.18    {
    3.19      val stream = new BufferedInputStream(new FileInputStream(file))
    3.20      val seq = new PagedSeq(

     4.1 --- a/src/Pure/General/sha1.scala	Fri Jul 20 21:05:47 2012 +0200
     4.2 +++ b/src/Pure/General/sha1.scala	Fri Jul 20 22:29:25 2012 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  package isabelle
     4.5  
     4.6  
     4.7 -import java.io.{File, FileInputStream}
     4.8 +import java.io.{File => JFile, FileInputStream}
     4.9  import java.security.MessageDigest
    4.10  
    4.11  
    4.12 @@ -30,7 +30,7 @@
    4.13      Digest(result.toString)
    4.14    }
    4.15  
    4.16 -  def digest(file: File): Digest =
    4.17 +  def digest(file: JFile): Digest =
    4.18    {
    4.19      val stream = new FileInputStream(file)
    4.20      val digest = MessageDigest.getInstance("SHA")

     5.1 --- a/src/Pure/System/build.scala	Fri Jul 20 21:05:47 2012 +0200
     5.2 +++ b/src/Pure/System/build.scala	Fri Jul 20 22:29:25 2012 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  package isabelle
     5.5  
     5.6  
     5.7 -import java.io.File
     5.8 +import java.io.{File => JFile}
     5.9  
    5.10  import scala.collection.mutable
    5.11  import scala.annotation.tailrec
    5.12 @@ -140,7 +140,7 @@
    5.13            { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
    5.14      }
    5.15  
    5.16 -    def parse_entries(root: File): List[Session_Entry] =
    5.17 +    def parse_entries(root: JFile): List[Session_Entry] =
    5.18      {
    5.19        val toks = syntax.scan(Standard_System.read_file(root))
    5.20        parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
    5.21 @@ -158,7 +158,7 @@
    5.22  
    5.23    private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    5.24  
    5.25 -  private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
    5.26 +  private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
    5.27    {
    5.28      (queue /: Parser.parse_entries(root))((queue1, entry) =>
    5.29        try {
    5.30 @@ -204,7 +204,7 @@
    5.31      else queue
    5.32    }
    5.33  
    5.34 -  private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
    5.35 +  private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
    5.36    {
    5.37      val dirs =
    5.38        split_lines(Standard_System.read_file(catalog)).

     6.1 --- a/src/Pure/System/isabelle_system.scala	Fri Jul 20 21:05:47 2012 +0200
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Fri Jul 20 22:29:25 2012 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  import java.lang.System
     6.5  import java.util.regex.Pattern
     6.6  import java.util.Locale
     6.7 -import java.io.{InputStream, OutputStream, File, BufferedReader, InputStreamReader,
     6.8 +import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
     6.9    BufferedWriter, OutputStreamWriter, IOException}
    6.10  import java.awt.{GraphicsEnvironment, Font}
    6.11  import java.awt.font.TextAttribute
    6.12 @@ -109,7 +109,7 @@
    6.13    def standard_path(path: Path): String = path.expand.implode
    6.14  
    6.15    def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
    6.16 -  def platform_file(path: Path): File = new File(platform_path(path))
    6.17 +  def platform_file(path: Path): JFile = new JFile(platform_path(path))
    6.18  
    6.19    def platform_file_url(raw_path: Path): String =
    6.20    {
    6.21 @@ -139,9 +139,9 @@
    6.22  
    6.23    /* source files */
    6.24  
    6.25 -  private def try_file(file: File) = if (file.isFile) Some(file) else None
    6.26 +  private def try_file(file: JFile) = if (file.isFile) Some(file) else None
    6.27  
    6.28 -  def source_file(path: Path): Option[File] =
    6.29 +  def source_file(path: Path): Option[JFile] =
    6.30    {
    6.31      if (path.is_absolute || path.is_current)
    6.32        try_file(platform_file(path))
    6.33 @@ -159,7 +159,7 @@
    6.34  
    6.35    /* plain execute */
    6.36  
    6.37 -  def execute_env(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
    6.38 +  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    6.39    {
    6.40      val cmdline =
    6.41        if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
    6.42 @@ -174,7 +174,7 @@
    6.43  
    6.44    /* managed process */
    6.45  
    6.46 -  class Managed_Process(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
    6.47 +  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    6.48    {
    6.49      private val params =
    6.50        List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
    6.51 @@ -241,7 +241,7 @@
    6.52  
    6.53    /* bash */
    6.54  
    6.55 -  def bash_env(cwd: File, env: Map[String, String], script: String): (String, String, Int) =
    6.56 +  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
    6.57    {
    6.58      Standard_System.with_tmp_file("isabelle_script") { script_file =>
    6.59        Standard_System.write_file(script_file, script)
    6.60 @@ -260,7 +260,7 @@
    6.61  
    6.62    def bash(script: String): (String, String, Int) = bash_env(null, null, script)
    6.63  
    6.64 -  class Bash_Job(cwd: File, env: Map[String, String], script: String)
    6.65 +  class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
    6.66    {
    6.67      private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
    6.68  

     7.1 --- a/src/Pure/System/options.scala	Fri Jul 20 21:05:47 2012 +0200
     7.2 +++ b/src/Pure/System/options.scala	Fri Jul 20 22:29:25 2012 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  package isabelle
     7.5  
     7.6  
     7.7 -import java.io.File
     7.8 +import java.io.{File => JFile}
     7.9  
    7.10  
    7.11  object Options
    7.12 @@ -49,7 +49,7 @@
    7.13          { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
    7.14      }
    7.15  
    7.16 -    def parse_entries(file: File): List[Options => Options] =
    7.17 +    def parse_entries(file: JFile): List[Options => Options] =
    7.18      {
    7.19        val toks = syntax.scan(Standard_System.read_file(file))
    7.20        parse_all(rep(entry), Token.reader(toks, file.toString)) match {

     8.1 --- a/src/Pure/System/standard_system.scala	Fri Jul 20 21:05:47 2012 +0200
     8.2 +++ b/src/Pure/System/standard_system.scala	Fri Jul 20 22:29:25 2012 +0200
     8.3 @@ -13,7 +13,7 @@
     8.4  import java.net.URL
     8.5  import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
     8.6    BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
     8.7 -  File, FileFilter, IOException}
     8.8 +  File => JFile, FileFilter, IOException}
     8.9  import java.nio.charset.Charset
    8.10  import java.util.zip.GZIPOutputStream
    8.11  
    8.12 @@ -114,9 +114,9 @@
    8.13    def slurp(stream: InputStream): String =
    8.14      slurp(new BufferedReader(new InputStreamReader(stream, charset)))
    8.15  
    8.16 -  def read_file(file: File): String = slurp(new FileInputStream(file))
    8.17 +  def read_file(file: JFile): String = slurp(new FileInputStream(file))
    8.18  
    8.19 -  def write_file(file: File, text: CharSequence, zip: Boolean = false)
    8.20 +  def write_file(file: JFile, text: CharSequence, zip: Boolean = false)
    8.21    {
    8.22      val stream1 = new FileOutputStream(file)
    8.23      val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    8.24 @@ -125,10 +125,10 @@
    8.25      finally { writer.close }
    8.26    }
    8.27  
    8.28 -  def eq_file(file1: File, file2: File): Boolean =
    8.29 +  def eq_file(file1: JFile, file2: JFile): Boolean =
    8.30      file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
    8.31  
    8.32 -  def copy_file(src: File, dst: File) =
    8.33 +  def copy_file(src: JFile, dst: JFile) =
    8.34      if (!eq_file(src, dst)) {
    8.35        val in = new FileInputStream(src)
    8.36        try {
    8.37 @@ -146,19 +146,19 @@
    8.38        finally { in.close }
    8.39      }
    8.40  
    8.41 -  def with_tmp_file[A](prefix: String)(body: File => A): A =
    8.42 +  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
    8.43    {
    8.44 -    val file = File.createTempFile(prefix, null)
    8.45 +    val file = JFile.createTempFile(prefix, null)
    8.46      file.deleteOnExit
    8.47      try { body(file) } finally { file.delete }
    8.48    }
    8.49  
    8.50    // FIXME handle (potentially cyclic) directory graph
    8.51 -  def find_files(start: File, ok: File => Boolean): List[File] =
    8.52 +  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
    8.53    {
    8.54 -    val files = new mutable.ListBuffer[File]
    8.55 -    val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
    8.56 -    def find_entry(entry: File)
    8.57 +    val files = new mutable.ListBuffer[JFile]
    8.58 +    val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
    8.59 +    def find_entry(entry: JFile)
    8.60      {
    8.61        if (ok(entry)) files += entry
    8.62        if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
    8.63 @@ -170,7 +170,7 @@
    8.64  
    8.65    /* shell processes */
    8.66  
    8.67 -  def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
    8.68 +  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    8.69    {
    8.70      val cmdline = new java.util.LinkedList[String]
    8.71      for (s <- args) cmdline.add(s)
    8.72 @@ -200,7 +200,7 @@
    8.73      (output, rc)
    8.74    }
    8.75  
    8.76 -  def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
    8.77 +  def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    8.78      : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
    8.79  
    8.80  
    8.81 @@ -215,10 +215,10 @@
    8.82        else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
    8.83        else error("Bad Cygwin installation: unknown root")
    8.84  
    8.85 -    val root_file = new File(root)
    8.86 -    if (!new File(root_file, "bin\\bash.exe").isFile ||
    8.87 -        !new File(root_file, "bin\\env.exe").isFile ||
    8.88 -        !new File(root_file, "bin\\tar.exe").isFile)
    8.89 +    val root_file = new JFile(root)
    8.90 +    if (!new JFile(root_file, "bin\\bash.exe").isFile ||
    8.91 +        !new JFile(root_file, "bin\\env.exe").isFile ||
    8.92 +        !new JFile(root_file, "bin\\tar.exe").isFile)
    8.93        error("Bad Cygwin installation: " + quote(root))
    8.94  
    8.95      root
    8.96 @@ -244,11 +244,11 @@
    8.97        val rest =
    8.98          posix_path match {
    8.99            case Cygdrive(drive, rest) =>
   8.100 -            result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + File.separator)
   8.101 +            result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
   8.102              rest
   8.103            case Named_Root(root, rest) =>
   8.104 -            result_path ++= File.separator
   8.105 -            result_path ++= File.separator
   8.106 +            result_path ++= JFile.separator
   8.107 +            result_path ++= JFile.separator
   8.108              result_path ++= root
   8.109              rest
   8.110            case path if path.startsWith("/") =>
   8.111 @@ -258,8 +258,8 @@
   8.112          }
   8.113        for (p <- space_explode('/', rest) if p != "") {
   8.114          val len = result_path.length
   8.115 -        if (len > 0 && result_path(len - 1) != File.separatorChar)
   8.116 -          result_path += File.separatorChar
   8.117 +        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
   8.118 +          result_path += JFile.separatorChar
   8.119          result_path ++= p
   8.120        }
   8.121        result_path.toString
   8.122 @@ -292,11 +292,11 @@
   8.123    def this_jdk_home(): String =
   8.124    {
   8.125      val java_home = System.getProperty("java.home")
   8.126 -    val home = new File(java_home)
   8.127 +    val home = new JFile(java_home)
   8.128      val parent = home.getParent
   8.129      val jdk_home =
   8.130        if (home.getName == "jre" && parent != null &&
   8.131 -          (new File(new File(parent, "bin"), "javac")).exists) parent
   8.132 +          (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
   8.133        else java_home
   8.134      posix_path(jdk_home)
   8.135    }

     9.1 --- a/src/Pure/System/system_channel.scala	Fri Jul 20 21:05:47 2012 +0200
     9.2 +++ b/src/Pure/System/system_channel.scala	Fri Jul 20 22:29:25 2012 +0200
     9.3 @@ -8,7 +8,8 @@
     9.4  package isabelle
     9.5  
     9.6  
     9.7 -import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
     9.8 +import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
     9.9 +  FileOutputStream, IOException}
    9.10  import java.net.{ServerSocket, InetAddress}
    9.11  
    9.12  

    10.1 --- a/src/Pure/Thy/thy_header.scala	Fri Jul 20 21:05:47 2012 +0200
    10.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Jul 20 22:29:25 2012 +0200
    10.3 @@ -12,7 +12,7 @@
    10.4  import scala.util.parsing.input.{Reader, CharSequenceReader}
    10.5  import scala.util.matching.Regex
    10.6  
    10.7 -import java.io.File
    10.8 +import java.io.{File => JFile}
    10.9  
   10.10  
   10.11  object Thy_Header extends Parse.Parser
   10.12 @@ -102,7 +102,7 @@
   10.13    def read(source: CharSequence): Thy_Header =
   10.14      read(new CharSequenceReader(source))
   10.15  
   10.16 -  def read(file: File): Thy_Header =
   10.17 +  def read(file: JFile): Thy_Header =
   10.18    {
   10.19      val reader = Scan.byte_reader(file)
   10.20      try { read(reader).map(Standard_System.decode_permissive_utf8) }

    11.1 --- a/src/Pure/Thy/thy_load.scala	Fri Jul 20 21:05:47 2012 +0200
    11.2 +++ b/src/Pure/Thy/thy_load.scala	Fri Jul 20 22:29:25 2012 +0200
    11.3 @@ -7,7 +7,7 @@
    11.4  package isabelle
    11.5  
    11.6  
    11.7 -import java.io.File
    11.8 +import java.io.{File => JFile}
    11.9  
   11.10  
   11.11  
   11.12 @@ -31,7 +31,7 @@
   11.13  
   11.14    def read_header(name: Document.Node.Name): Thy_Header =
   11.15    {
   11.16 -    val file = new File(name.node)
   11.17 +    val file = new JFile(name.node)
   11.18      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   11.19      Thy_Header.read(file)
   11.20    }

    12.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Fri Jul 20 21:05:47 2012 +0200
    12.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Fri Jul 20 22:29:25 2012 +0200
    12.3 @@ -9,7 +9,7 @@
    12.4  
    12.5  import isabelle._
    12.6  
    12.7 -import java.io.File
    12.8 +import java.io.{File => JFile}
    12.9  
   12.10  import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
   12.11  

    13.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Fri Jul 20 21:05:47 2012 +0200
    13.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Fri Jul 20 22:29:25 2012 +0200
    13.3 @@ -9,7 +9,7 @@
    13.4  
    13.5  import isabelle._
    13.6  
    13.7 -import java.io.{File, IOException}
    13.8 +import java.io.{File => JFile, IOException}
    13.9  import javax.swing.text.Segment
   13.10  
   13.11  import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
   13.12 @@ -65,7 +65,7 @@
   13.13          case None => None
   13.14        }
   13.15      } getOrElse {
   13.16 -      val file = new File(name.node)  // FIXME load URL via jEdit VFS (!?)
   13.17 +      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
   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/Tools/jEdit/src/scala_console.scala	Fri Jul 20 21:05:47 2012 +0200
    14.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Fri Jul 20 22:29:25 2012 +0200
    14.3 @@ -15,7 +15,7 @@
    14.4  import org.gjt.sp.jedit.MiscUtilities
    14.5  
    14.6  import java.lang.System
    14.7 -import java.io.{File, OutputStream, Writer, PrintWriter}
    14.8 +import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
    14.9  
   14.10  import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
   14.11  import scala.tools.nsc.interpreter.IMain
   14.12 @@ -30,11 +30,11 @@
   14.13    {
   14.14      def find_jars(start: String): List[String] =
   14.15        if (start != null)
   14.16 -        Standard_System.find_files(new File(start),
   14.17 +        Standard_System.find_files(new JFile(start),
   14.18            entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
   14.19        else Nil
   14.20      val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
   14.21 -    path.mkString(File.pathSeparator)
   14.22 +    path.mkString(JFile.pathSeparator)
   14.23    }
   14.24  
   14.25