# HG changeset patch # User wenzelm # Date 1440090917 -7200 # Node ID 1d7a7e33fd6789da35a79af65c17eab1208863e2 # Parent ea00d17eba3b49458d19314d13ecb98cf00e6a05 tuned signature, according to ML version; diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Pure/General/file.scala Thu Aug 20 19:15:17 2015 +0200 @@ -17,6 +17,27 @@ object File { + /* system path representations */ + + def standard_path(path: Path): String = path.expand.implode + + def platform_path(path: Path): String = Isabelle_System.jvm_path(standard_path(path)) + def platform_file(path: Path): JFile = new JFile(platform_path(path)) + + def platform_file_url(raw_path: Path): String = + { + val path = raw_path.expand + require(path.is_absolute) + val s = platform_path(path).replaceAll(" ", "%20") + if (!Platform.is_windows) "file://" + s + else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') + else "file:///" + s.replace('\\', '/') + } + + def shell_path(path: Path): String = "'" + standard_path(path) + "'" + def shell_path(file: JFile): String = "'" + Isabelle_System.posix_path(file) + "'" + + /* directory content */ def read_dir(dir: Path): List[String] = diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Pure/General/path.scala Thu Aug 20 19:15:17 2015 +0200 @@ -205,7 +205,7 @@ /* platform file */ - def file: JFile = Isabelle_System.platform_file(this) + def file: JFile = File.platform_file(this) def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory } diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Pure/System/isabelle_system.scala Thu Aug 20 19:15:17 2015 +0200 @@ -219,27 +219,6 @@ catch { case _: MalformedURLException => posix_path(name) } - /* misc path specifications */ - - def standard_path(path: Path): String = path.expand.implode - - def platform_path(path: Path): String = jvm_path(standard_path(path)) - def platform_file(path: Path): JFile = new JFile(platform_path(path)) - - def platform_file_url(raw_path: Path): String = - { - val path = raw_path.expand - require(path.is_absolute) - val s = platform_path(path).replaceAll(" ", "%20") - if (!Platform.is_windows) "file://" + s - else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') - else "file:///" + s.replace('\\', '/') - } - - def shell_path(path: Path): String = "'" + standard_path(path) + "'" - def shell_path(file: JFile): String = "'" + posix_path(file) + "'" - - /* source files of Isabelle/ML bootstrap */ def source_file(path: Path): Option[Path] = @@ -259,8 +238,8 @@ def mkdirs(path: Path): Unit = if (!path.is_dir) { - bash("perl -e \"use File::Path make_path; make_path(" + shell_path(path) + ");\"") - if (!path.is_dir) error("Failed to create directory: " + quote(platform_path(path))) + bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"") + if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } @@ -320,7 +299,7 @@ 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") + List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script") private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*) @@ -390,7 +369,7 @@ { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs - platform_file(path) + File.platform_file(path) } def tmp_file[A](name: String, ext: String = ""): JFile = @@ -523,7 +502,7 @@ catch { case _: SecurityException => false } } match { case Some(dir) => - val file = standard_path(dir + Path.basic(name)) + val file = File.standard_path(dir + Path.basic(name)) process_output(execute(true, (List(file) ::: args.toList): _*)) case None => ("Unknown Isabelle tool: " + name, 2) } @@ -533,10 +512,10 @@ bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = - bash("exec \"$PDF_VIEWER\" '" + standard_path(arg) + "' >/dev/null 2>/dev/null &") + bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &") def hg(cmd_line: String, cwd: Path = Path.current): Bash_Result = - bash("cd " + shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line) + bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line) /** Isabelle resources **/ diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Pure/Tools/build.scala Thu Aug 20 19:15:17 2015 +0200 @@ -591,7 +591,7 @@ })) private val env = - Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output), + Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output), (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> Isabelle_System.posix_path(args_file)) diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Pure/Tools/check_source.scala --- a/src/Pure/Tools/check_source.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Pure/Tools/check_source.scala Thu Aug 20 19:15:17 2015 +0200 @@ -41,7 +41,7 @@ def check_hg(root: Path) { Output.writeln("Checking " + root + " ...") - Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error + Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check_error for { file <- Isabelle_System.hg("manifest", root).check_error.out_lines if file.endsWith(".thy") || file.endsWith(".ML") diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Pure/Tools/main.scala Thu Aug 20 19:15:17 2015 +0200 @@ -102,11 +102,11 @@ Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") val jedit_settings = - Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS"))) + Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))) val more_args = if (args.isEmpty) - Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) + Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) else args @@ -114,11 +114,8 @@ update_environment() - System.setProperty("jedit.home", - Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist"))) - - System.setProperty("scala.home", - Isabelle_System.platform_path(Path.explode("$SCALA_HOME"))) + System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) + System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) val jedit = Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Thu Aug 20 19:15:17 2015 +0200 @@ -54,10 +54,10 @@ { node.getUserObject match { case Text_File(_, path) => - PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path)) + PIDE.editor.goto_file(true, view, File.platform_path(path)) case Documentation(_, _, path) => if (path.is_file) - PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path)) + PIDE.editor.goto_file(true, view, File.platform_path(path)) else { Future.fork { try { Doc.view(path) } diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Aug 20 19:15:17 2015 +0200 @@ -225,7 +225,7 @@ if (Path.is_wellformed(source_name)) { if (Path.is_valid(source_name)) { val path = Path.explode(source_name) - Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path)) + Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path)) } else None } diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 20 19:15:17 2015 +0200 @@ -308,8 +308,7 @@ { val name1 = if (name.startsWith("idea-icons/")) { - val file = - Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar")) + val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar")) "jar:" + file + "!/" + name } else name diff -r ea00d17eba3b -r 1d7a7e33fd67 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Thu Aug 20 17:41:50 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Aug 20 19:15:17 2015 +0200 @@ -56,14 +56,14 @@ { val path = source_path.expand if (dir == "" || path.is_absolute) - MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path)) + MiscUtilities.resolveSymlinks(File.platform_path(path)) else if (path.is_current) dir else { val vfs = VFSManager.getVFSForPath(dir) if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks( - vfs.constructPath(dir, Isabelle_System.platform_path(path))) - else vfs.constructPath(dir, Isabelle_System.standard_path(path)) + vfs.constructPath(dir, File.platform_path(path))) + else vfs.constructPath(dir, File.standard_path(path)) } }