--- 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)