# HG changeset patch # User wenzelm # Date 1356962301 -3600 # Node ID ead5714cc4805954326c84df3090b9887a4d5a44 # Parent 1fe68f1c3069beb6370d424b94597e82e3d651ec tuned signature -- eliminated obsolete Standard_System; diff -r 1fe68f1c3069 -r ead5714cc480 src/Pure/System/gui_setup.scala --- a/src/Pure/System/gui_setup.scala Mon Dec 31 13:49:01 2012 +0100 +++ b/src/Pure/System/gui_setup.scala Mon Dec 31 14:58:21 2012 +0100 @@ -41,7 +41,7 @@ // values if (Platform.is_windows) - text.append("Cygwin root: " + Standard_System.cygwin_root() + "\n") + text.append("Cygwin root: " + Isabelle_System.cygwin_root() + "\n") text.append("JVM name: " + Platform.jvm_name + "\n") text.append("JVM platform: " + Platform.jvm_platform + "\n") text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n") diff -r 1fe68f1c3069 -r ead5714cc480 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Dec 31 13:49:01 2012 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Dec 31 14:58:21 2012 +0100 @@ -21,20 +21,41 @@ object Isabelle_System { - /** implicit state **/ - - private case class State(standard_system: Standard_System, settings: Map[String, String]) + /** bootstrap information **/ - @volatile private var _state: Option[State] = None - - private def check_state(): State = + def jdk_home(): String = { - if (_state.isEmpty) init() // unsynchronized check - _state.get + val java_home = System.getProperty("java.home") + val home = new JFile(java_home) + val parent = home.getParent + if (home.getName == "jre" && parent != null && + (new JFile(new JFile(parent, "bin"), "javac")).exists) parent + else java_home } - def standard_system: Standard_System = check_state().standard_system - def settings: Map[String, String] = check_state().settings + def cygwin_root(): String = + { + require(Platform.is_windows) + + val cygwin_root1 = System.getenv("CYGWIN_ROOT") + val cygwin_root2 = System.getProperty("cygwin.root") + + if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1 + else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2 + else error("Cannot determine Cygwin root directory") + } + + + + /** implicit settings environment **/ + + @volatile private var _settings: Option[Map[String, String]] = None + + def settings(): Map[String, String] = + { + if (_settings.isEmpty) init() // unsynchronized check + _settings.get + } /* isabelle_home precedence: @@ -42,14 +63,13 @@ (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(this_isabelle_home: String = null) = synchronized { - if (_state.isEmpty) { + def init(this_isabelle_home: String = null): Unit = synchronized { + if (_settings.isEmpty) { import scala.collection.JavaConversions._ - val standard_system = new Standard_System val settings = { - val env0 = sys.env + ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home()) + val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())) val user_home = System.getProperty("user.home") val env = @@ -69,7 +89,7 @@ File.with_tmp_file("settings") { dump => val shell_prefix = - if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l") + if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash", "-l") else Nil val cmdline = shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) @@ -85,7 +105,7 @@ entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } } - _state = Some(State(standard_system, settings)) + _settings = Some(settings) } } @@ -103,11 +123,64 @@ /** file-system operations **/ - /* path specifications */ + /* 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 ++= (Library.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 posix_path + + + /* posix_path */ + + def posix_path(jvm_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]):\\*(.*)""") + + jvm_path.replace('/', '\\') match { + case Platform_Root(rest) => "/" + rest.replace('\\', '/') + case Drive(letter, rest) => + "/cygdrive/" + Library.lowercase(letter) + + (if (rest == "") "" else "/" + rest.replace('\\', '/')) + case path => path.replace('\\', '/') + } + } + else jvm_path + + + /* misc path specifications */ def standard_path(path: Path): String = path.expand.implode - def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path)) + def platform_path(path: Path): String = jvm_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) def platform_file_url(raw_path: Path): String = @@ -120,8 +193,6 @@ else "file:///" + s.replace('\\', '/') } - def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path) - /* source files of Isabelle/ML bootstrap */ @@ -179,7 +250,7 @@ def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = { val cmdline = - if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args + if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ++ args else args val env1 = if (env == null) settings else settings ++ env raw_execute(cwd, env1, redirect, cmdline: _*) diff -r 1fe68f1c3069 -r ead5714cc480 src/Pure/System/standard_system.scala --- a/src/Pure/System/standard_system.scala Mon Dec 31 13:49:01 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -/* Title: Pure/System/standard_system.scala - Author: Makarius - -Standard system operations, with basic Cygwin/Posix compatibility. -*/ - -package isabelle - -import java.lang.System -import java.util.regex.Pattern -import java.net.URL -import java.io.{File => JFile} - -import scala.util.matching.Regex - - -object Standard_System -{ - /* cygwin_root */ - - def cygwin_root(): String = - { - val cygwin_root1 = System.getenv("CYGWIN_ROOT") - val cygwin_root2 = System.getProperty("cygwin.root") - val root = - if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1 - else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2 - else error("Bad Cygwin installation: unknown root") - - val root_file = new JFile(root) - if (!new JFile(root_file, "bin\\bash.exe").isFile || - !new JFile(root_file, "bin\\env.exe").isFile || - !new JFile(root_file, "bin\\tar.exe").isFile) - error("Bad Cygwin installation: " + quote(root)) - - root - } -} - - -class Standard_System -{ - /* platform_root */ - - val platform_root = if (Platform.is_windows) Standard_System.cygwin_root() else "/" - - - /* 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 ++= (Library.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 ++= platform_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 */ - - private val Platform_Root = new Regex("(?i)" + - Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""") - - private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") - - def posix_path(jvm_path: String): String = - if (Platform.is_windows) { - jvm_path.replace('/', '\\') match { - case Platform_Root(rest) => "/" + rest.replace('\\', '/') - case Drive(letter, rest) => - "/cygdrive/" + Library.lowercase(letter) + - (if (rest == "") "" else "/" + rest.replace('\\', '/')) - case path => path.replace('\\', '/') - } - } - else jvm_path - - - /* JDK home of running JVM */ - - def this_jdk_home(): String = - { - val java_home = System.getProperty("java.home") - val home = new JFile(java_home) - val parent = home.getParent - val jdk_home = - if (home.getName == "jre" && parent != null && - (new JFile(new JFile(parent, "bin"), "javac")).exists) parent - else java_home - posix_path(jdk_home) - } -} diff -r 1fe68f1c3069 -r ead5714cc480 src/Pure/build-jars --- a/src/Pure/build-jars Mon Dec 31 13:49:01 2012 +0100 +++ b/src/Pure/build-jars Mon Dec 31 14:58:21 2012 +0100 @@ -54,7 +54,6 @@ System/options.scala System/platform.scala System/session.scala - System/standard_system.scala System/swing_thread.scala System/system_channel.scala System/utf8.scala