# HG changeset patch # User wenzelm # Date 1343390999 -7200 # Node ID 49afe0e921630129212dbabfbaba7754d64acb5c # Parent b3b092d0a9fe2b9684c6b86a0ff3f6faef6c7c9a simplified Path vs. JVM File operations; diff -r b3b092d0a9fe -r 49afe0e92163 src/Pure/General/path.scala --- 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 } diff -r b3b092d0a9fe -r 49afe0e92163 src/Pure/General/position.scala --- 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) diff -r b3b092d0a9fe -r 49afe0e92163 src/Pure/System/build.scala --- 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) diff -r b3b092d0a9fe -r 49afe0e92163 src/Pure/System/isabelle_system.scala --- 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 } diff -r b3b092d0a9fe -r 49afe0e92163 src/Pure/System/options.scala --- 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 }