simplified Path vs. JVM File operations;

--- a/src/Pure/General/path.scala	Fri Jul 27 13:33:34 2012 +0200
+++ b/src/Pure/General/path.scala	Fri Jul 27 14:09:59 2012 +0200
@@ -175,7 +175,14 @@
   }
 
 
+  /* source position */
+
+  def position: Position.T = Position.File(implode)
+
+
   /* platform file */
 
   def file: JFile = Isabelle_System.platform_file(this)
+  def is_file: Boolean = file.isFile
+  def is_dir: Boolean = file.isDirectory
 }

--- a/src/Pure/General/position.scala	Fri Jul 27 13:33:34 2012 +0200
+++ b/src/Pure/General/position.scala	Fri Jul 27 14:09:59 2012 +0200
@@ -20,9 +20,6 @@
   val File = new Properties.String(Isabelle_Markup.FILE)
   val Id = new Properties.Long(Isabelle_Markup.ID)
 
-  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
   {
     def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)

--- a/src/Pure/System/build.scala	Fri Jul 27 13:33:34 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 27 14:09:59 2012 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.io.{File => JFile, BufferedInputStream, FileInputStream,
+import java.io.{BufferedInputStream, FileInputStream,
   BufferedReader, InputStreamReader, IOException}
 import java.util.zip.GZIPInputStream
 
@@ -138,10 +138,10 @@
           { 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: JFile): List[Session_Entry] =
+    def parse_entries(root: Path): List[Session_Entry] =
     {
       val toks = syntax.scan(File.read(root))
-      parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
+      parse_all(rep(session_entry), Token.reader(toks, root.implode)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
@@ -156,7 +156,7 @@
 
   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
 
-  private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
+  private def sessions_root(options: Options, dir: Path, root: Path, queue: Session.Queue)
     : Session.Queue =
   {
     (queue /: Parser.parse_entries(root))((queue1, entry) =>
@@ -202,20 +202,20 @@
       catch {
         case ERROR(msg) =>
           error(msg + "\nThe error(s) above occurred in session entry " +
-            quote(entry.base_name) + Position.str_of(Position.file(root)))
+            quote(entry.base_name) + Position.str_of(root.position))
       })
   }
 
   private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
     : Session.Queue =
   {
-    val root = (dir + ROOT).file
-    if (root.isFile) sessions_root(options, dir, root, queue)
-    else if (strict) error("Bad session root file: " + quote(root.toString))
+    val root = dir + ROOT
+    if (root.is_file) sessions_root(options, dir, root, queue)
+    else if (strict) error("Bad session root file: " + root.toString)
     else queue
   }
 
-  private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
+  private def sessions_catalog(options: Options, dir: Path, catalog: Path, queue: Session.Queue)
     : Session.Queue =
   {
     val dirs =
@@ -223,12 +223,12 @@
     (queue /: dirs)((queue1, dir1) =>
       try {
         val dir2 = dir + Path.explode(dir1)
-        if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
+        if (dir2.is_dir) sessions_dir(options, true, dir2, queue1)
         else error("Bad session directory: " + dir2.toString)
       }
       catch {
         case ERROR(msg) =>
-          error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
+          error(msg + "\nThe error(s) above occurred in session catalog " + catalog.toString)
       })
   }
 
@@ -240,9 +240,8 @@
     for (dir <- Isabelle_System.components()) {
       queue = sessions_dir(options, false, dir, queue)
 
-      val catalog = (dir + SESSIONS).file
-      if (catalog.isFile)
-        queue = sessions_catalog(options, dir, catalog, queue)
+      val catalog = dir + SESSIONS
+      if (catalog.is_file) queue = sessions_catalog(options, dir, catalog, queue)
     }
 
     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
@@ -317,7 +316,7 @@
 
   /* jobs */
 
-  private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
+  private class Job(dir: Path, env: Map[String, String], script: String, args: String,
     output: Path, do_output: Boolean)
   {
     private val args_file = File.tmp_file("args")
@@ -325,7 +324,7 @@
     File.write(args_file, args)
 
     private val (thread, result) =
-      Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
+      Simple_Thread.future("build") { Isabelle_System.bash_env(dir.file, env1, script) }
 
     def terminate: Unit = thread.interrupt
     def is_finished: Boolean = result.is_finished
@@ -337,7 +336,7 @@
     options: Options, verbose: Boolean, browser_info: Path): Job =
   {
     // global browser info dir
-    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
+    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
     {
       browser_info.file.mkdirs()
       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
@@ -350,7 +349,6 @@
 
     val parent = info.parent.getOrElse("")
 
-    val cwd = info.dir.file
     val env =
       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
     val script =
@@ -390,7 +388,7 @@
           (do_output, (options, (verbose, (browser_info, (parent,
             (name, info.theories)))))))
     }
-    new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
+    new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output)
   }
 
 
@@ -508,7 +506,7 @@
 
                 val current =
                 {
-                  input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
+                  input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
                     case Some(dir) =>
                       check_stamps(dir, name) match {
                         case Some((s, h)) => s == make_stamp(name) && (h || !do_output)

--- a/src/Pure/System/isabelle_system.scala	Fri Jul 27 13:33:34 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Jul 27 14:09:59 2012 +0200
@@ -129,10 +129,10 @@
   def try_read(paths: Seq[Path]): String =
   {
     val buf = new StringBuilder
-    for {
-      path <- paths
-      file = platform_file(path) if file.isFile
-    } { buf.append(File.read(file)); buf.append('\n') }
+    for (path <- paths if path.is_file) {
+      buf.append(File.read(path))
+      buf.append('\n')
+    }
     buf.toString
   }
 

--- a/src/Pure/System/options.scala	Fri Jul 27 13:33:34 2012 +0200
+++ b/src/Pure/System/options.scala	Fri Jul 27 14:09:59 2012 +0200
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import java.io.{File => JFile}
-
-
 object Options
 {
   type Spec = (String, Option[String])
@@ -54,9 +51,9 @@
         { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
     }
 
-    def parse_entries(file: JFile): List[Options => Options] =
+    def parse_entries(file: Path): List[Options => Options] =
     {
-      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
+      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
@@ -70,12 +67,11 @@
     var options = empty
     for {
       dir <- Isabelle_System.components()
-      file = (dir + OPTIONS).file
-      if file.isFile
+      file = dir + OPTIONS if file.is_file
       entry <- Parser.parse_entries(file)
     } {
       try { options = entry(options) }
-      catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) }
+      catch { case ERROR(msg) => error(msg + Position.str_of(file.position)) }
     }
     options
   }