# HG changeset patch
# User wenzelm
# Date 1342816165 -7200
# Node ID 0d2114eb412a7ffae75ccc1cea8fb8a72a15ebb8
# Parent  623607c5a40f1cf69dff83e05ce6fbdaa802a063
more explicit java.io.{File => JFile};

diff -r 623607c5a40f -r 0d2114eb412a src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/General/path.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -8,7 +8,7 @@
 package isabelle
 
 
-import java.io.File
+import java.io.{File => JFile}
 
 import scala.util.matching.Regex
 
@@ -168,5 +168,5 @@
 
   /* platform file */
 
-  def file: File = Isabelle_System.platform_file(this)
+  def file: JFile = Isabelle_System.platform_file(this)
 }
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/General/position.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.io.{File => JFile}
+
+
 object Position
 {
   type T = Properties.T
@@ -17,8 +20,8 @@
   val File = new Properties.String(Isabelle_Markup.FILE)
   val Id = new Properties.Long(Isabelle_Markup.ID)
 
-  def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
-  def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
+  def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString))
+  def line_file(i: Int, f: JFile): T = Line(i) ::: file(f)
 
   object Range
   {
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/General/scan.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -12,7 +12,7 @@
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
 
-import java.io.{File, BufferedInputStream, FileInputStream}
+import java.io.{File => JFile, BufferedInputStream, FileInputStream}
 
 
 object Scan
@@ -422,7 +422,7 @@
 
   abstract class Byte_Reader extends Reader[Char] { def close: Unit }
 
-  def byte_reader(file: File): Byte_Reader =
+  def byte_reader(file: JFile): Byte_Reader =
   {
     val stream = new BufferedInputStream(new FileInputStream(file))
     val seq = new PagedSeq(
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/General/sha1.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -8,7 +8,7 @@
 package isabelle
 
 
-import java.io.{File, FileInputStream}
+import java.io.{File => JFile, FileInputStream}
 import java.security.MessageDigest
 
 
@@ -30,7 +30,7 @@
     Digest(result.toString)
   }
 
-  def digest(file: File): Digest =
+  def digest(file: JFile): Digest =
   {
     val stream = new FileInputStream(file)
     val digest = MessageDigest.getInstance("SHA")
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.io.File
+import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.annotation.tailrec
@@ -140,7 +140,7 @@
           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
     }
 
-    def parse_entries(root: File): List[Session_Entry] =
+    def parse_entries(root: JFile): List[Session_Entry] =
     {
       val toks = syntax.scan(Standard_System.read_file(root))
       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
@@ -158,7 +158,7 @@
 
   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
 
-  private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
+  private def sessions_root(dir: Path, root: JFile, queue: Session.Queue): Session.Queue =
   {
     (queue /: Parser.parse_entries(root))((queue1, entry) =>
       try {
@@ -204,7 +204,7 @@
     else queue
   }
 
-  private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
+  private def sessions_catalog(dir: Path, catalog: JFile, queue: Session.Queue): Session.Queue =
   {
     val dirs =
       split_lines(Standard_System.read_file(catalog)).
diff -r 623607c5a40f -r 0d2114eb412a 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) }
 
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/System/options.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.io.File
+import java.io.{File => JFile}
 
 
 object Options
@@ -49,7 +49,7 @@
         { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
     }
 
-    def parse_entries(file: File): List[Options => Options] =
+    def parse_entries(file: JFile): List[Options => Options] =
     {
       val toks = syntax.scan(Standard_System.read_file(file))
       parse_all(rep(entry), Token.reader(toks, file.toString)) match {
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/System/standard_system.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -13,7 +13,7 @@
 import java.net.URL
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
-  File, FileFilter, IOException}
+  File => JFile, FileFilter, IOException}
 import java.nio.charset.Charset
 import java.util.zip.GZIPOutputStream
 
@@ -114,9 +114,9 @@
   def slurp(stream: InputStream): String =
     slurp(new BufferedReader(new InputStreamReader(stream, charset)))
 
-  def read_file(file: File): String = slurp(new FileInputStream(file))
+  def read_file(file: JFile): String = slurp(new FileInputStream(file))
 
-  def write_file(file: File, text: CharSequence, zip: Boolean = false)
+  def write_file(file: JFile, text: CharSequence, zip: Boolean = false)
   {
     val stream1 = new FileOutputStream(file)
     val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
@@ -125,10 +125,10 @@
     finally { writer.close }
   }
 
-  def eq_file(file1: File, file2: File): Boolean =
+  def eq_file(file1: JFile, file2: JFile): Boolean =
     file1.getCanonicalPath == file2.getCanonicalPath  // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
 
-  def copy_file(src: File, dst: File) =
+  def copy_file(src: JFile, dst: JFile) =
     if (!eq_file(src, dst)) {
       val in = new FileInputStream(src)
       try {
@@ -146,19 +146,19 @@
       finally { in.close }
     }
 
-  def with_tmp_file[A](prefix: String)(body: File => A): A =
+  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
   {
-    val file = File.createTempFile(prefix, null)
+    val file = JFile.createTempFile(prefix, null)
     file.deleteOnExit
     try { body(file) } finally { file.delete }
   }
 
   // FIXME handle (potentially cyclic) directory graph
-  def find_files(start: File, ok: File => Boolean): List[File] =
+  def find_files(start: JFile, ok: JFile => Boolean): List[JFile] =
   {
-    val files = new mutable.ListBuffer[File]
-    val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
-    def find_entry(entry: File)
+    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)
@@ -170,7 +170,7 @@
 
   /* shell processes */
 
-  def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
+  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline = new java.util.LinkedList[String]
     for (s <- args) cmdline.add(s)
@@ -200,7 +200,7 @@
     (output, rc)
   }
 
-  def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
+  def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
     : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
 
 
@@ -215,10 +215,10 @@
       else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
       else error("Bad Cygwin installation: unknown root")
 
-    val root_file = new File(root)
-    if (!new File(root_file, "bin\\bash.exe").isFile ||
-        !new File(root_file, "bin\\env.exe").isFile ||
-        !new File(root_file, "bin\\tar.exe").isFile)
+    val root_file = new JFile(root)
+    if (!new JFile(root_file, "bin\\bash.exe").isFile ||
+        !new JFile(root_file, "bin\\env.exe").isFile ||
+        !new JFile(root_file, "bin\\tar.exe").isFile)
       error("Bad Cygwin installation: " + quote(root))
 
     root
@@ -244,11 +244,11 @@
       val rest =
         posix_path match {
           case Cygdrive(drive, rest) =>
-            result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + File.separator)
+            result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
             rest
           case Named_Root(root, rest) =>
-            result_path ++= File.separator
-            result_path ++= File.separator
+            result_path ++= JFile.separator
+            result_path ++= JFile.separator
             result_path ++= root
             rest
           case path if path.startsWith("/") =>
@@ -258,8 +258,8 @@
         }
       for (p <- space_explode('/', rest) if p != "") {
         val len = result_path.length
-        if (len > 0 && result_path(len - 1) != File.separatorChar)
-          result_path += File.separatorChar
+        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
+          result_path += JFile.separatorChar
         result_path ++= p
       }
       result_path.toString
@@ -292,11 +292,11 @@
   def this_jdk_home(): String =
   {
     val java_home = System.getProperty("java.home")
-    val home = new File(java_home)
+    val home = new JFile(java_home)
     val parent = home.getParent
     val jdk_home =
       if (home.getName == "jre" && parent != null &&
-          (new File(new File(parent, "bin"), "javac")).exists) parent
+          (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
       else java_home
     posix_path(jdk_home)
   }
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/System/system_channel.scala
--- a/src/Pure/System/system_channel.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/System/system_channel.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -8,7 +8,8 @@
 package isabelle
 
 
-import java.io.{InputStream, OutputStream, File, FileInputStream, FileOutputStream, IOException}
+import java.io.{InputStream, OutputStream, File => JFile, FileInputStream,
+  FileOutputStream, IOException}
 import java.net.{ServerSocket, InetAddress}
 
 
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -12,7 +12,7 @@
 import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.util.matching.Regex
 
-import java.io.File
+import java.io.{File => JFile}
 
 
 object Thy_Header extends Parse.Parser
@@ -102,7 +102,7 @@
   def read(source: CharSequence): Thy_Header =
     read(new CharSequenceReader(source))
 
-  def read(file: File): Thy_Header =
+  def read(file: JFile): Thy_Header =
   {
     val reader = Scan.byte_reader(file)
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
diff -r 623607c5a40f -r 0d2114eb412a src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.io.File
+import java.io.{File => JFile}
 
 
 
@@ -31,7 +31,7 @@
 
   def read_header(name: Document.Node.Name): Thy_Header =
   {
-    val file = new File(name.node)
+    val file = new JFile(name.node)
     if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     Thy_Header.read(file)
   }
diff -r 623607c5a40f -r 0d2114eb412a src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.io.File
+import java.io.{File => JFile}
 
 import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
 
diff -r 623607c5a40f -r 0d2114eb412a src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.io.{File, IOException}
+import java.io.{File => JFile, IOException}
 import javax.swing.text.Segment
 
 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
@@ -65,7 +65,7 @@
         case None => None
       }
     } getOrElse {
-      val file = new File(name.node)  // FIXME load URL via jEdit VFS (!?)
+      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
       Thy_Header.read(file)
     }
diff -r 623607c5a40f -r 0d2114eb412a src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -15,7 +15,7 @@
 import org.gjt.sp.jedit.MiscUtilities
 
 import java.lang.System
-import java.io.{File, OutputStream, Writer, PrintWriter}
+import java.io.{File => JFile, OutputStream, Writer, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
 import scala.tools.nsc.interpreter.IMain
@@ -30,11 +30,11 @@
   {
     def find_jars(start: String): List[String] =
       if (start != null)
-        Standard_System.find_files(new File(start),
+        Standard_System.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)
-    path.mkString(File.pathSeparator)
+    path.mkString(JFile.pathSeparator)
   }