--- a/src/Pure/General/file.scala Wed Jun 30 12:46:49 2021 +0200
+++ b/src/Pure/General/file.scala Wed Jun 30 13:25:35 2021 +0200
@@ -15,13 +15,11 @@
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
-import java.util.regex.Pattern
import java.util.EnumSet
import org.tukaani.xz.{XZInputStream, XZOutputStream}
import scala.collection.mutable
-import scala.util.matching.Regex
object File
@@ -31,20 +29,7 @@
def standard_path(path: Path): String = path.expand.implode
def standard_path(platform_path: String): String =
- if (Platform.is_windows) {
- val Platform_Root = new Regex("(?i)" +
- Pattern.quote(Isabelle_System.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
+ Isabelle_Env.standard_path(Isabelle_System.cygwin_root(), platform_path)
def standard_path(file: JFile): String = standard_path(file.getPath)
@@ -60,36 +45,8 @@
/* 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.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
+ Isabelle_Env.platform_path(Isabelle_System.cygwin_root(), standard_path)
def platform_path(path: Path): String = platform_path(standard_path(path))
def platform_file(path: Path): JFile = new JFile(platform_path(path))
--- a/src/Pure/System/isabelle_env.scala Wed Jun 30 12:46:49 2021 +0200
+++ b/src/Pure/System/isabelle_env.scala Wed Jun 30 13:25:35 2021 +0200
@@ -8,10 +8,13 @@
package isabelle
+import java.util.regex.Pattern
import java.util.{HashMap, LinkedList, List => JList, Map => JMap}
import java.io.{File => JFile}
import java.nio.file.Files
+import scala.util.matching.Regex
+
object Isabelle_Env
{
@@ -44,6 +47,55 @@
/** Support for Cygwin as POSIX emulation on Windows **/
+ /* system path representations */
+
+ def standard_path(cygwin_root: String, platform_path: String): String =
+ if (Platform.is_windows) {
+ val Platform_Root = new Regex("(?i)" + Pattern.quote(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 platform_path(cygwin_root: String, standard_path: String): String =
+ if (Platform.is_windows) {
+ val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
+ val Named_Root = new Regex("//+([^/]*)(.*)")
+
+ 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 ++= 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
+
+
/* symlink emulation */
def cygwin_link(content: String, target: JFile): Unit =
@@ -182,7 +234,6 @@
if (Platform.is_windows) {
val root = bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
cygwin_init(isabelle_root1, root)
- _settings = JMap.of("CYGWIN_ROOT", root)
root
}
else ""
@@ -196,7 +247,7 @@
val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
})
- env_default("ISABELLE_JDK_HOME", File.standard_path(jdk_home()))
+ env_default("ISABELLE_JDK_HOME", standard_path(cygwin_root1, jdk_home()))
env_default("HOME", System.getProperty("user.home", ""))
env_default("ISABELLE_APP", System.getProperty("isabelle.app", ""))
@@ -207,7 +258,7 @@
if (Platform.is_windows) {
cmd.add(cygwin_root1 + "\\bin\\bash")
cmd.add("-l")
- cmd.add(File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
+ cmd.add(standard_path(cygwin_root1, isabelle_root1 + "\\bin\\isabelle"))
} else {
cmd.add(isabelle_root1 + "/bin/isabelle")
}
--- a/src/Pure/System/isabelle_system.scala Wed Jun 30 12:46:49 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Jun 30 13:25:35 2021 +0200
@@ -27,7 +27,7 @@
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
- def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+ def cygwin_root(): String = getenv("CYGWIN_ROOT")
/* services */