1.1 --- a/src/Pure/General/path.scala	Fri Jul 27 13:33:34 2012 +0200
     1.2 +++ b/src/Pure/General/path.scala	Fri Jul 27 14:09:59 2012 +0200
     1.3 @@ -175,7 +175,14 @@
     1.4    }
     1.5  
     1.6  
     1.7 +  /* source position */
     1.8 +
     1.9 +  def position: Position.T = Position.File(implode)
    1.10 +
    1.11 +
    1.12    /* platform file */
    1.13  
    1.14    def file: JFile = Isabelle_System.platform_file(this)
    1.15 +  def is_file: Boolean = file.isFile
    1.16 +  def is_dir: Boolean = file.isDirectory
    1.17  }

     2.1 --- a/src/Pure/General/position.scala	Fri Jul 27 13:33:34 2012 +0200
     2.2 +++ b/src/Pure/General/position.scala	Fri Jul 27 14:09:59 2012 +0200
     2.3 @@ -20,9 +20,6 @@
     2.4    val File = new Properties.String(Isabelle_Markup.FILE)
     2.5    val Id = new Properties.Long(Isabelle_Markup.ID)
     2.6  
     2.7 -  def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString))
     2.8 -  def line_file(i: Int, f: JFile): T = Line(i) ::: file(f)
     2.9 -
    2.10    object Range
    2.11    {
    2.12      def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)

     3.1 --- a/src/Pure/System/build.scala	Fri Jul 27 13:33:34 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Fri Jul 27 14:09:59 2012 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  package isabelle
     3.5  
     3.6  
     3.7 -import java.io.{File => JFile, BufferedInputStream, FileInputStream,
     3.8 +import java.io.{BufferedInputStream, FileInputStream,
     3.9    BufferedReader, InputStreamReader, IOException}
    3.10  import java.util.zip.GZIPInputStream
    3.11  
    3.12 @@ -138,10 +138,10 @@
    3.13            { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
    3.14      }
    3.15  
    3.16 -    def parse_entries(root: JFile): List[Session_Entry] =
    3.17 +    def parse_entries(root: Path): List[Session_Entry] =
    3.18      {
    3.19        val toks = syntax.scan(File.read(root))
    3.20 -      parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
    3.21 +      parse_all(rep(session_entry), Token.reader(toks, root.implode)) match {
    3.22          case Success(result, _) => result
    3.23          case bad => error(bad.toString)
    3.24        }
    3.25 @@ -156,7 +156,7 @@
    3.26  
    3.27    private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    3.28  
    3.29 -  private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
    3.30 +  private def sessions_root(options: Options, dir: Path, root: Path, queue: Session.Queue)
    3.31      : Session.Queue =
    3.32    {
    3.33      (queue /: Parser.parse_entries(root))((queue1, entry) =>
    3.34 @@ -202,20 +202,20 @@
    3.35        catch {
    3.36          case ERROR(msg) =>
    3.37            error(msg + "\nThe error(s) above occurred in session entry " +
    3.38 -            quote(entry.base_name) + Position.str_of(Position.file(root)))
    3.39 +            quote(entry.base_name) + Position.str_of(root.position))
    3.40        })
    3.41    }
    3.42  
    3.43    private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
    3.44      : Session.Queue =
    3.45    {
    3.46 -    val root = (dir + ROOT).file
    3.47 -    if (root.isFile) sessions_root(options, dir, root, queue)
    3.48 -    else if (strict) error("Bad session root file: " + quote(root.toString))
    3.49 +    val root = dir + ROOT
    3.50 +    if (root.is_file) sessions_root(options, dir, root, queue)
    3.51 +    else if (strict) error("Bad session root file: " + root.toString)
    3.52      else queue
    3.53    }
    3.54  
    3.55 -  private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
    3.56 +  private def sessions_catalog(options: Options, dir: Path, catalog: Path, queue: Session.Queue)
    3.57      : Session.Queue =
    3.58    {
    3.59      val dirs =
    3.60 @@ -223,12 +223,12 @@
    3.61      (queue /: dirs)((queue1, dir1) =>
    3.62        try {
    3.63          val dir2 = dir + Path.explode(dir1)
    3.64 -        if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
    3.65 +        if (dir2.is_dir) sessions_dir(options, true, dir2, queue1)
    3.66          else error("Bad session directory: " + dir2.toString)
    3.67        }
    3.68        catch {
    3.69          case ERROR(msg) =>
    3.70 -          error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
    3.71 +          error(msg + "\nThe error(s) above occurred in session catalog " + catalog.toString)
    3.72        })
    3.73    }
    3.74  
    3.75 @@ -240,9 +240,8 @@
    3.76      for (dir <- Isabelle_System.components()) {
    3.77        queue = sessions_dir(options, false, dir, queue)
    3.78  
    3.79 -      val catalog = (dir + SESSIONS).file
    3.80 -      if (catalog.isFile)
    3.81 -        queue = sessions_catalog(options, dir, catalog, queue)
    3.82 +      val catalog = dir + SESSIONS
    3.83 +      if (catalog.is_file) queue = sessions_catalog(options, dir, catalog, queue)
    3.84      }
    3.85  
    3.86      for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
    3.87 @@ -317,7 +316,7 @@
    3.88  
    3.89    /* jobs */
    3.90  
    3.91 -  private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
    3.92 +  private class Job(dir: Path, env: Map[String, String], script: String, args: String,
    3.93      output: Path, do_output: Boolean)
    3.94    {
    3.95      private val args_file = File.tmp_file("args")
    3.96 @@ -325,7 +324,7 @@
    3.97      File.write(args_file, args)
    3.98  
    3.99      private val (thread, result) =
   3.100 -      Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
   3.101 +      Simple_Thread.future("build") { Isabelle_System.bash_env(dir.file, env1, script) }
   3.102  
   3.103      def terminate: Unit = thread.interrupt
   3.104      def is_finished: Boolean = result.is_finished
   3.105 @@ -337,7 +336,7 @@
   3.106      options: Options, verbose: Boolean, browser_info: Path): Job =
   3.107    {
   3.108      // global browser info dir
   3.109 -    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
   3.110 +    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   3.111      {
   3.112        browser_info.file.mkdirs()
   3.113        File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   3.114 @@ -350,7 +349,6 @@
   3.115  
   3.116      val parent = info.parent.getOrElse("")
   3.117  
   3.118 -    val cwd = info.dir.file
   3.119      val env =
   3.120        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output))
   3.121      val script =
   3.122 @@ -390,7 +388,7 @@
   3.123            (do_output, (options, (verbose, (browser_info, (parent,
   3.124              (name, info.theories)))))))
   3.125      }
   3.126 -    new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
   3.127 +    new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output)
   3.128    }
   3.129  
   3.130  
   3.131 @@ -508,7 +506,7 @@
   3.132  
   3.133                  val current =
   3.134                  {
   3.135 -                  input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
   3.136 +                  input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   3.137                      case Some(dir) =>
   3.138                        check_stamps(dir, name) match {
   3.139                          case Some((s, h)) => s == make_stamp(name) && (h || !do_output)

     4.1 --- a/src/Pure/System/isabelle_system.scala	Fri Jul 27 13:33:34 2012 +0200
     4.2 +++ b/src/Pure/System/isabelle_system.scala	Fri Jul 27 14:09:59 2012 +0200
     4.3 @@ -129,10 +129,10 @@
     4.4    def try_read(paths: Seq[Path]): String =
     4.5    {
     4.6      val buf = new StringBuilder
     4.7 -    for {
     4.8 -      path <- paths
     4.9 -      file = platform_file(path) if file.isFile
    4.10 -    } { buf.append(File.read(file)); buf.append('\n') }
    4.11 +    for (path <- paths if path.is_file) {
    4.12 +      buf.append(File.read(path))
    4.13 +      buf.append('\n')
    4.14 +    }
    4.15      buf.toString
    4.16    }
    4.17  

     5.1 --- a/src/Pure/System/options.scala	Fri Jul 27 13:33:34 2012 +0200
     5.2 +++ b/src/Pure/System/options.scala	Fri Jul 27 14:09:59 2012 +0200
     5.3 @@ -7,9 +7,6 @@
     5.4  package isabelle
     5.5  
     5.6  
     5.7 -import java.io.{File => JFile}
     5.8 -
     5.9 -
    5.10  object Options
    5.11  {
    5.12    type Spec = (String, Option[String])
    5.13 @@ -54,9 +51,9 @@
    5.14          { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
    5.15      }
    5.16  
    5.17 -    def parse_entries(file: JFile): List[Options => Options] =
    5.18 +    def parse_entries(file: Path): List[Options => Options] =
    5.19      {
    5.20 -      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match {
    5.21 +      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
    5.22          case Success(result, _) => result
    5.23          case bad => error(bad.toString)
    5.24        }
    5.25 @@ -70,12 +67,11 @@
    5.26      var options = empty
    5.27      for {
    5.28        dir <- Isabelle_System.components()
    5.29 -      file = (dir + OPTIONS).file
    5.30 -      if file.isFile
    5.31 +      file = dir + OPTIONS if file.is_file
    5.32        entry <- Parser.parse_entries(file)
    5.33      } {
    5.34        try { options = entry(options) }
    5.35 -      catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) }
    5.36 +      catch { case ERROR(msg) => error(msg + Position.str_of(file.position)) }
    5.37      }
    5.38      options
    5.39    }