--- a/Admin/build Sun Jun 28 15:01:29 2009 +0200
+++ b/Admin/build Sun Jun 28 18:47:22 2009 +0200
@@ -8,6 +8,9 @@
PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH"
PATH="/home/scala/current/bin:$PATH"
+if [ -z "$SCALA_HOME" ]; then
+ export SCALA_HOME="$(dirname "$(dirname "$(type -p scalac)")")"
+fi
## directory layout
@@ -32,7 +35,7 @@
all all modules below
browser graph browser (requires jdk)
doc documentation (requires latex and rail)
- jars JVM components (requires jdk and scala)
+ jars Scala/JVM components (requires scala)
EOF
exit 1
@@ -93,13 +96,13 @@
function build_jars ()
{
echo "###"
- echo "### Building JVM components ..."
+ echo "### Building Scala/JVM components ..."
echo "###"
- type -p scalac >/dev/null || fail "Scala compiler unavailable"
+ [ -z "$SCALA_HOME" ] && fail "Scala unavailable: unknown SCALA_HOME"
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
- "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
+ "$ISABELLE_TOOL" make jars || fail "Failed to build isabelle-scala.jar"
popd >/dev/null
}
--- a/src/Pure/IsaMakefile Sun Jun 28 15:01:29 2009 +0200
+++ b/src/Pure/IsaMakefile Sun Jun 28 18:47:22 2009 +0200
@@ -121,23 +121,28 @@
General/position.scala General/scan.scala General/swing.scala \
General/symbol.scala General/xml.scala General/yxml.scala \
Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \
- System/cygwin.scala System/isabelle_process.scala \
- System/isabelle_system.scala Thy/completion.scala \
- Thy/thy_header.scala Tools/isabelle_syntax.scala
+ System/cygwin.scala System/gui_setup.scala \
+ System/isabelle_process.scala System/isabelle_system.scala \
+ System/platform.scala Thy/completion.scala Thy/thy_header.scala \
+ Tools/isabelle_syntax.scala
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
+ISABELLE_SCALA = $(ISABELLE_HOME)/lib/classes/isabelle-scala.jar
-jar: $(SCALA_TARGET)
+jars: $(SCALA_TARGET)
$(SCALA_TARGET): $(SCALA_FILES)
@rm -rf classes && mkdir classes
- scalac -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
- scaladoc -d classes $(SCALA_FILES)
+ $(SCALA_HOME)/bin/scalac -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
+ $(SCALA_HOME)/bin/scaladoc -d classes $(SCALA_FILES)
@cp $(SCALA_FILES) classes/isabelle
@mkdir -p `dirname $@`
- @cd classes; jar cf `jvmpath $@` isabelle
+ @cd classes; jar cfe `jvmpath $@` isabelle.GUI_Setup isabelle
+ @cd classes; jar xf `jvmpath $(SCALA_HOME)/lib/scala-swing.jar`; \
+ cp $(SCALA_HOME)/lib/scala-library.jar $(ISABELLE_SCALA); \
+ jar ufe `jvmpath $(ISABELLE_SCALA)` isabelle.GUI_Setup isabelle scala
@rm -rf classes
-clean-jar:
- @rm -f $(SCALA_TARGET)
+clean-jars:
+ @rm -f $(SCALA_TARGET) $(ISABELLE_SCALA)
--- a/src/Pure/System/cygwin.scala Sun Jun 28 15:01:29 2009 +0200
+++ b/src/Pure/System/cygwin.scala Sun Jun 28 18:47:22 2009 +0200
@@ -7,6 +7,7 @@
package isabelle
import java.lang.reflect.Method
+import java.io.File
object Cygwin
@@ -75,10 +76,31 @@
/* Cygwin installation */
+ // old-style mount points (Cygwin 1.5)
private val CYGWIN_MOUNTS = "Software\\Cygnus Solutions\\Cygwin\\mounts v2"
- def cygdrive(): Option[String] = query_registry(CYGWIN_MOUNTS, "cygdrive prefix")
- def root(): Option[String] = query_registry(CYGWIN_MOUNTS + "\\/", "native")
+ // new-style setup (Cygwin 1.7)
+ private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup"
+ private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup" // !?
+ def config(): (String, String) =
+ {
+ query_registry(CYGWIN_SETUP1, "rootdir") match {
+ case Some(root) => (root, "/cygdrive")
+ case None =>
+ val root =
+ query_registry(CYGWIN_MOUNTS + "\\/", "native") getOrElse "C:\\cygwin"
+ val cygdrive =
+ query_registry(CYGWIN_MOUNTS, "cygdrive prefix") getOrElse "cygdrive"
+ (root, cygdrive)
+ }
+ }
+
+
+ /* basic sanity check */
+
+ def check(root: String): Boolean =
+ new File(root + "\\bin\\bash.exe").isFile &&
+ new File(root + "\\bin\\env.exe").isFile
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/gui_setup.scala Sun Jun 28 18:47:22 2009 +0200
@@ -0,0 +1,41 @@
+/* Title: Pure/System/gui_setup.scala
+ Author: Makarius
+
+GUI for basic system setup.
+*/
+
+package isabelle
+
+import javax.swing.UIManager
+
+import scala.swing._
+import scala.swing.event._
+
+
+object GUI_Setup extends GUIApplication
+{
+ def main(args: Array[String]) =
+ {
+ Swing.later {
+ UIManager.setLookAndFeel(Platform.look_and_feel)
+ top.pack()
+ top.visible = true
+ }
+ }
+
+ def top = new MainFrame {
+ title = "Isabelle setup"
+ val ok = new Button { text = "OK" }
+
+ contents = new BoxPanel(Orientation.Vertical) {
+ contents += ok
+ border = scala.swing.Swing.EmptyBorder(20, 20, 20, 20)
+ }
+
+ listenTo(ok)
+ reactions += {
+ case ButtonClicked(`ok`) => System.exit(0)
+ }
+ }
+}
+
--- a/src/Pure/System/isabelle_system.scala Sun Jun 28 15:01:29 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Sun Jun 28 18:47:22 2009 +0200
@@ -19,42 +19,6 @@
val charset = "UTF-8"
- /* platform identification */
-
- val is_cygwin = System.getProperty("os.name").startsWith("Windows")
-
- private val X86 = new Regex("i.86|x86")
- private val X86_64 = new Regex("amd64|x86_64")
- private val Sparc = new Regex("sparc")
- private val PPC = new Regex("PowerPC|ppc")
-
- private val Solaris = new Regex("SunOS|Solaris")
- private val Linux = new Regex("Linux")
- private val Darwin = new Regex("Mac OS X")
- private val Cygwin = new Regex("Windows.*")
-
- val default_platform: Option[String] =
- {
- val name =
- java.lang.System.getProperty("os.name") match {
- case Solaris() => "solaris"
- case Linux() => "linux"
- case Darwin() => "darwin"
- case Cygwin() => "cygwin"
- case _ => ""
- }
- val arch =
- java.lang.System.getProperty("os.arch") match {
- case X86() | X86_64() => "x86"
- case Sparc() => "sparc"
- case PPC() => "ppc"
- case _ => ""
- }
- if (arch == "" || name == "") None
- else Some(arch + "-" + name)
- }
-
-
/* shell processes */
private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
@@ -98,9 +62,9 @@
private val (platform_root, drive_prefix, shell_prefix) =
{
- if (Isabelle_System.is_cygwin) {
- val root = Cygwin.root() getOrElse "C:\\cygwin"
- val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
+ if (Platform.is_windows) {
+ val (root, drive) = Cygwin.config()
+ if (!Cygwin.check(root)) error("Bad Cygwin installation: " + root)
val shell = List(root + "\\bin\\bash", "-l")
(root, drive, shell)
}
@@ -220,7 +184,7 @@
val result_path = new StringBuilder
val rest =
expand_path(isabelle_path) match {
- case Cygdrive(drive, rest) if Isabelle_System.is_cygwin =>
+ case Cygdrive(drive, rest) if Platform.is_windows =>
result_path ++= (drive + ":" + File.separator)
rest
case path if path.startsWith("/") =>
@@ -248,7 +212,7 @@
def isabelle_path(platform_path: String): String =
{
- if (Isabelle_System.is_cygwin) {
+ if (Platform.is_windows) {
platform_path.replace('/', '\\') match {
case Platform_Root(rest) => "/" + rest.replace('\\', '/')
case Drive(letter, rest) =>
@@ -286,7 +250,7 @@
def execute(redirect: Boolean, args: String*): Process =
{
val cmdline =
- if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args
+ if (Platform.is_windows) List(platform_path("/bin/env")) ++ args
else args
Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
}
@@ -325,7 +289,7 @@
{
// blocks until writer is ready
val stream =
- if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream
+ if (Platform.is_windows) execute(false, "cat", fifo).getInputStream
else new FileInputStream(fifo)
new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/platform.scala Sun Jun 28 18:47:22 2009 +0200
@@ -0,0 +1,69 @@
+/* Title: Pure/System/platform.scala
+ Author: Makarius
+
+Raw platform identification.
+*/
+
+package isabelle
+
+import javax.swing.UIManager
+
+import scala.util.matching.Regex
+
+
+object Platform
+{
+ /* main OS variants */
+
+ val is_macos = System.getProperty("os.name") == "Mac OS X"
+ val is_windows = System.getProperty("os.name").startsWith("Windows")
+
+
+ /* Isabelle platform identifiers */
+
+ private val Solaris = new Regex("SunOS|Solaris")
+ private val Linux = new Regex("Linux")
+ private val Darwin = new Regex("Mac OS X")
+ private val Cygwin = new Regex("Windows.*")
+
+ private val X86 = new Regex("i.86|x86")
+ private val X86_64 = new Regex("amd64|x86_64")
+ private val Sparc = new Regex("sparc")
+ private val PPC = new Regex("PowerPC|ppc")
+
+ // main default, optional 64bit variant
+ val defaults: Option[(String, Option[String])] =
+ {
+ (java.lang.System.getProperty("os.name") match {
+ case Solaris() => Some("solaris")
+ case Linux() => Some("linux")
+ case Darwin() => Some("darwin")
+ case Cygwin() => Some("cygwin")
+ case _ => None
+ }) match {
+ case Some(name) =>
+ java.lang.System.getProperty("os.arch") match {
+ case X86() => Some(("x86-" + name, None))
+ case X86_64() => Some(("x86-" + name, if (is_windows) None else Some("x86_64-" + name)))
+ case Sparc() => Some(("sparc-" + name, None))
+ case PPC() => Some(("ppc-" + name, None))
+ }
+ case None => None
+ }
+ }
+
+
+ /* Swing look-and-feel */
+
+ def look_and_feel(): String =
+ {
+ if (is_windows || is_macos) UIManager.getSystemLookAndFeelClassName()
+ else {
+ UIManager.getInstalledLookAndFeels().find(laf => laf.getName == "Nimbus") match {
+ case None => UIManager.getCrossPlatformLookAndFeelClassName()
+ case Some(laf) => laf.getClassName
+ }
+ }
+ }
+}
+