# HG changeset patch # User wenzelm # Date 1625052335 -7200 # Node ID 1f1e490dd25164761f335b5d8f01689cdd4af6f9 # Parent 4d64bc3878677dd1e5ce50f212bfdde54d05cd4d clarified modules; avoid initial use of _settings during init; diff -r 4d64bc387867 -r 1f1e490dd251 src/Pure/General/file.scala --- 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)) diff -r 4d64bc387867 -r 1f1e490dd251 src/Pure/System/isabelle_env.scala --- 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") } diff -r 4d64bc387867 -r 1f1e490dd251 src/Pure/System/isabelle_system.scala --- 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 */