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)