# HG changeset patch # User wenzelm # Date 1440097727 -7200 # Node ID 89effcb342dfda69fd45930f903cc5c571611ecb # Parent 2fc5a44346b5ab2531c04cbe0e15f4a06698c7af clarified modules, like ML version; diff -r 2fc5a44346b5 -r 89effcb342df src/Pure/General/file.scala --- a/src/Pure/General/file.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Pure/General/file.scala Thu Aug 20 21:08:47 2015 +0200 @@ -10,21 +10,85 @@ import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} +import java.net.{URL, URLDecoder, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} +import java.util.regex.Pattern import scala.collection.mutable +import scala.util.matching.Regex object File { - /* system path representations */ + /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode - def platform_path(path: Path): String = Isabelle_System.jvm_path(standard_path(path)) + def standard_path(platform_path: String): String = + if (Platform.is_windows) { + val Platform_Root = new Regex("(?i)" + + Pattern.quote(Isabelle_System.get_cygwin_root()) + """(?:\\+|\z)(.*)""") + val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") + + platform_path.replace('/', '\\') match { + case Platform_Root(rest) => "/" + rest.replace('\\', '/') + case Drive(letter, rest) => + "/cygdrive/" + Word.lowercase(letter) + + (if (rest == "") "" else "/" + rest.replace('\\', '/')) + case path => path.replace('\\', '/') + } + } + else platform_path + + def standard_path(file: JFile): String = standard_path(file.getPath) + + def standard_url(name: String): String = + try { + val url = new URL(name) + if (url.getProtocol == "file") + standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name)) + else name + } + catch { case _: MalformedURLException => standard_path(name) } + + + /* platform path (Windows or Posix) */ + + private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") + private val Named_Root = new Regex("//+([^/]*)(.*)") + + def platform_path(standard_path: String): String = + if (Platform.is_windows) { + val result_path = new StringBuilder + val rest = + standard_path match { + case Cygdrive(drive, rest) => + result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) + rest + case Named_Root(root, rest) => + result_path ++= JFile.separator + result_path ++= JFile.separator + result_path ++= root + rest + case path if path.startsWith("/") => + result_path ++= Isabelle_System.get_cygwin_root() + path + case path => path + } + for (p <- space_explode('/', rest) if p != "") { + val len = result_path.length + if (len > 0 && result_path(len - 1) != JFile.separatorChar) + result_path += JFile.separatorChar + result_path ++= p + } + result_path.toString + } + else standard_path + + def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) - def platform_file_url(raw_path: Path): String = + def platform_url(raw_path: Path): String = { val path = raw_path.expand require(path.is_absolute) @@ -34,8 +98,11 @@ else "file:///" + s.replace('\\', '/') } + + /* shell path (bash) */ + def shell_path(path: Path): String = "'" + standard_path(path) + "'" - def shell_path(file: JFile): String = "'" + Isabelle_System.posix_path(file) + "'" + def shell_path(file: JFile): String = "'" + standard_path(file) + "'" /* directory content */ @@ -172,4 +239,3 @@ def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) } - diff -r 2fc5a44346b5 -r 89effcb342df src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Pure/PIDE/protocol.scala Thu Aug 20 21:08:47 2015 +0200 @@ -368,7 +368,7 @@ variant(List( { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Deps(header) => - val master_dir = Isabelle_System.posix_path_url(name.master_dir) + val master_dir = File.standard_url(name.master_dir) val theory = Long_Name.base_name(name.theory) val imports = header.imports.map({ case (a, _) => a.node }) val keywords = header.keywords.map({ case (a, b, _) => (a, b) }) diff -r 2fc5a44346b5 -r 89effcb342df src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Pure/System/isabelle_system.scala Thu Aug 20 21:08:47 2015 +0200 @@ -8,13 +8,9 @@ package isabelle -import java.util.regex.Pattern import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes -import java.net.{URL, URLDecoder, MalformedURLException} - -import scala.util.matching.Regex object Isabelle_System @@ -91,7 +87,7 @@ default( default( - default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())), + default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") @@ -154,70 +150,6 @@ /** file-system operations **/ - /* jvm_path */ - - private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") - private val Named_Root = new Regex("//+([^/]*)(.*)") - - def jvm_path(posix_path: String): String = - if (Platform.is_windows) { - val result_path = new StringBuilder - val rest = - posix_path match { - case Cygdrive(drive, rest) => - result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) - rest - case Named_Root(root, rest) => - result_path ++= JFile.separator - result_path ++= JFile.separator - result_path ++= root - rest - case path if path.startsWith("/") => - result_path ++= get_cygwin_root() - path - case path => path - } - for (p <- space_explode('/', rest) if p != "") { - val len = result_path.length - if (len > 0 && result_path(len - 1) != JFile.separatorChar) - result_path += JFile.separatorChar - result_path ++= p - } - result_path.toString - } - else posix_path - - - /* posix_path */ - - def posix_path(jvm_path: String): String = - if (Platform.is_windows) { - val Platform_Root = new Regex("(?i)" + - Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""") - val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") - - jvm_path.replace('/', '\\') match { - case Platform_Root(rest) => "/" + rest.replace('\\', '/') - case Drive(letter, rest) => - "/cygdrive/" + Word.lowercase(letter) + - (if (rest == "") "" else "/" + rest.replace('\\', '/')) - case path => path.replace('\\', '/') - } - } - else jvm_path - - def posix_path(file: JFile): String = posix_path(file.getPath) - - def posix_path_url(name: String): String = - try { - val url = new URL(name) - if (url.getProtocol == "file") - posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name)) - else name - } - catch { case _: MalformedURLException => posix_path(name) } - - /* source files of Isabelle/ML bootstrap */ def source_file(path: Path): Option[Path] = @@ -381,7 +313,7 @@ { with_tmp_file("isabelle_script") { script_file => File.write(script_file, script) - val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file)) + val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file)) proc.stdin.close val limited = new Limited_Progress(proc, progress_limit) diff -r 2fc5a44346b5 -r 89effcb342df src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Pure/Tools/build.scala Thu Aug 20 21:08:47 2015 +0200 @@ -586,14 +586,14 @@ pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))))( (command_timings, (do_output, (info.options, (verbose, (browser_info, - (info.document_files, (Isabelle_System.posix_path(graph_file), (parent, + (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, theories))))))))))) })) private val env = 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)) + File.standard_path(args_file)) private val script = if (is_pure(name)) { diff -r 2fc5a44346b5 -r 89effcb342df src/Pure/Tools/build_doc.scala --- a/src/Pure/Tools/build_doc.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Pure/Tools/build_doc.scala Thu Aug 20 21:08:47 2015 +0200 @@ -50,7 +50,7 @@ Build.build( options.bool.update("browser_info", false). string.update("document", "pdf"). - string.update("document_output", Isabelle_System.posix_path(output)), + string.update("document_output", File.standard_path(output)), progress, clean_build = true, max_jobs = max_jobs, system_mode = system_mode, sessions = sessions) if (rc2 == 0) { diff -r 2fc5a44346b5 -r 89effcb342df src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Pure/Tools/main.scala Thu Aug 20 21:08:47 2015 +0200 @@ -228,8 +228,8 @@ val upd = if (Platform.is_windows) List( - "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home), - "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user), + "ISABELLE_HOME" -> File.platform_path(isabelle_home), + "ISABELLE_HOME_USER" -> File.platform_path(isabelle_home_user), "INI_DIR" -> "") else List( diff -r 2fc5a44346b5 -r 89effcb342df src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Tools/jEdit/src/active.scala Thu Aug 20 21:08:47 2015 +0200 @@ -34,7 +34,7 @@ val graph_file = Isabelle_System.tmp_file("graph") File.write(graph_file, XML.content(body)) Isabelle_System.bash_env(null, - Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)), + Map("GRAPH_FILE" -> File.standard_path(graph_file)), "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &") } diff -r 2fc5a44346b5 -r 89effcb342df src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Aug 20 21:08:47 2015 +0200 @@ -83,7 +83,7 @@ val name = session_args().last val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name) content.copy(known_theories = - content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_)))) + content.known_theories.mapValues(name => name.map(File.platform_path(_)))) } } diff -r 2fc5a44346b5 -r 89effcb342df src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 20 20:36:06 2015 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 20 21:08:47 2015 +0200 @@ -308,7 +308,7 @@ { val name1 = if (name.startsWith("idea-icons/")) { - val file = File.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar")) + val file = File.platform_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar")) "jar:" + file + "!/" + name } else name