uniform treatment of bootstrap directories;
Isabelle_System.init() includes Cygwin.init(), e.g. for situations without isabelle.Main;
tuned;
--- a/src/Pure/General/file.scala Wed Sep 30 14:49:39 2015 +0200
+++ b/src/Pure/General/file.scala Wed Sep 30 20:02:39 2015 +0200
@@ -27,7 +27,7 @@
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)(.*)""")
+ Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
platform_path.replace('/', '\\') match {
@@ -71,7 +71,7 @@
result_path ++= root
rest
case path if path.startsWith("/") =>
- result_path ++= Isabelle_System.get_cygwin_root()
+ result_path ++= Isabelle_System.cygwin_root()
path
case path => path
}
--- a/src/Pure/System/cygwin.scala Wed Sep 30 14:49:39 2015 +0200
+++ b/src/Pure/System/cygwin.scala Wed Sep 30 20:02:39 2015 +0200
@@ -15,73 +15,51 @@
object Cygwin
{
- /** Cygwin init (e.g. after extraction via 7zip) **/
-
- def init()
- {
- val isabelle_home0 = System.getenv("ISABELLE_HOME")
- if (isabelle_home0 == null || isabelle_home0 == "") {
+ /* init (e.g. after extraction via 7zip) */
- /* isabelle_home */
-
- val isabelle_home = System.getProperty("isabelle.home", "")
-
- if (isabelle_home == "")
- error("Unknown Isabelle home directory")
-
- if (!(new JFile(isabelle_home)).isDirectory)
- error("Bad Isabelle home directory: " + quote(isabelle_home))
+ def init(isabelle_home: String, cygwin_root: String)
+ {
+ require(Platform.is_windows)
- def execute(args: String*)
- {
- val cwd = new JFile(isabelle_home)
- val env = Map("CYGWIN" -> "nodosfilewarning")
- val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
- val (output, rc) = Isabelle_System.process_output(proc)
- if (rc != 0) error(output)
- }
+ def execute(args: String*)
+ {
+ val cwd = new JFile(isabelle_home)
+ val env = Map("CYGWIN" -> "nodosfilewarning")
+ val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+ val (output, rc) = Isabelle_System.process_output(proc)
+ if (rc != 0) error(output)
+ }
-
- /* cygwin_root */
-
- val cygwin_root = isabelle_home + "\\contrib\\cygwin"
- if ((new JFile(cygwin_root)).isDirectory)
- System.setProperty("cygwin.root", cygwin_root)
-
+ val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
+ val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
- /* init */
-
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+ if (uninitialized) {
+ val symlinks =
+ {
+ val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
+ Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+ }
+ @tailrec def recover_symlinks(list: List[String]): Unit =
+ {
+ list match {
+ case Nil | List("") =>
+ case link :: content :: rest =>
+ val path = (new JFile(isabelle_home, link)).toPath
- if (uninitialized) {
- val symlinks =
- {
- val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
- Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+ val writer = Files.newBufferedWriter(path, UTF8.charset)
+ try { writer.write("!<symlink>" + content + "\u0000") }
+ finally { writer.close }
+
+ Files.setAttribute(path, "dos:system", true)
+
+ recover_symlinks(rest)
+ case _ => error("Unbalanced symlinks list")
}
- @tailrec def recover_symlinks(list: List[String]): Unit =
- {
- list match {
- case Nil | List("") =>
- case link :: content :: rest =>
- val path = (new JFile(isabelle_home, link)).toPath
-
- val writer = Files.newBufferedWriter(path, UTF8.charset)
- try { writer.write("!<symlink>" + content + "\u0000") }
- finally { writer.close }
+ }
+ recover_symlinks(symlinks)
- Files.setAttribute(path, "dos:system", true)
-
- recover_symlinks(rest)
- case _ => error("Unbalanced symlinks list")
- }
- }
- recover_symlinks(symlinks)
-
- execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
- execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
- }
+ execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+ execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
}
}
}
--- a/src/Pure/System/isabelle_system.scala Wed Sep 30 14:49:39 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Sep 30 20:02:39 2015 +0200
@@ -29,17 +29,20 @@
else java_home
}
- private def find_cygwin_root(cygwin_root0: String = ""): String =
+ def bootstrap_directory(
+ preference: String, envar: String, property: String, description: String): String =
{
- require(Platform.is_windows)
+ def check(s: String): Option[String] =
+ if (s != null && s != "") Some(s) else None
- val cygwin_root1 = System.getenv("CYGWIN_ROOT")
- val cygwin_root2 = System.getProperty("cygwin.root")
+ val value =
+ check(preference) orElse // explicit argument
+ check(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
+ check(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
+ error("Unknown " + description + " directory")
- if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0
- else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
- else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
- else error("Cannot determine Cygwin root directory")
+ if ((new JFile(value)).isDirectory) value
+ else error("Bad " + description + " directory " + quote(value))
}
@@ -54,21 +57,22 @@
_settings.get
}
- /*
- Isabelle home precedence:
- (1) isabelle_home as explicit argument
- (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
- (3) isabelle.home system property (e.g. via JVM application boot process)
- */
def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
if (_settings.isEmpty) {
import scala.collection.JavaConversions._
+ val isabelle_home1 =
+ bootstrap_directory(isabelle_home, "ISABELLE_HOME", "isabelle.home", "Isabelle home")
+
+ val cygwin_root1 =
+ if (Platform.is_windows)
+ bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
+ else ""
+
def set_cygwin_root()
{
if (Platform.is_windows)
- _settings = Some(_settings.getOrElse(Map.empty) +
- ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
+ _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
}
set_cygwin_root()
@@ -81,7 +85,7 @@
{
val temp_windows =
{
- val temp = System.getenv("TEMP")
+ val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
}
val user_home = System.getProperty("user.home", "")
@@ -95,27 +99,15 @@
"ISABELLE_APP" -> "true")
}
- val system_home =
- if (isabelle_home != null && isabelle_home != "") isabelle_home
- else
- env.get("ISABELLE_HOME") match {
- case None | Some("") =>
- val path = System.getProperty("isabelle.home", "")
- if (path == "") error("Unknown Isabelle home directory")
- else path
- case Some(path) => path
- }
-
val settings =
{
val dump = JFile.createTempFile("settings", null)
dump.deleteOnExit
try {
val shell_prefix =
- if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
- else Nil
+ if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
val cmdline =
- shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
+ shell_prefix ::: List(isabelle_home1 + "/bin/isabelle", "getenv", "-d", dump.toString)
val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
if (rc != 0) error(output)
@@ -146,7 +138,7 @@
else error("Undefined Isabelle environment variable: " + quote(name))
}
- def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+ def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
@@ -218,7 +210,7 @@
def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: args.toList
else args
val env1 = if (env == null) settings else settings ++ env
raw_execute(cwd, env1, redirect, cmdline: _*)
@@ -298,7 +290,7 @@
def kill(signal: String, group_pid: String): (String, Int) =
{
val bash =
- if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\bash.exe")
+ if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
process_output(raw_execute(null, null, true, cmdline: _*))
--- a/src/Pure/Tools/main.scala Wed Sep 30 14:49:39 2015 +0200
+++ b/src/Pure/Tools/main.scala Wed Sep 30 20:02:39 2015 +0200
@@ -19,10 +19,6 @@
val start =
{
try {
- /* system init */
-
- if (Platform.is_windows) Cygwin.init()
-
Isabelle_System.init()