# HG changeset patch # User wenzelm # Date 1443636159 -7200 # Node ID e00e1bf23d03e5e575eb854eaf42fea0a3f70838 # Parent b18f83985215d0795c8e9c420f9c1d41d5fddeab uniform treatment of bootstrap directories; Isabelle_System.init() includes Cygwin.init(), e.g. for situations without isabelle.Main; tuned; diff -r b18f83985215 -r e00e1bf23d03 src/Pure/General/file.scala --- 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 } diff -r b18f83985215 -r e00e1bf23d03 src/Pure/System/cygwin.scala --- 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("!" + 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("!" + 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") } } } diff -r b18f83985215 -r e00e1bf23d03 src/Pure/System/isabelle_system.scala --- 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: _*)) diff -r b18f83985215 -r e00e1bf23d03 src/Pure/Tools/main.scala --- 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()