# HG changeset patch
# User wenzelm
# Date 1246207642 -7200
# Node ID 2ce69d6d558147e1a7c8047ac44b54339363b860
# Parent  beeaa1ed1f478d512903e5e262c420e3bfad31c4# Parent  92993da74973224dafafc38197279b77b8988fb0
merged

diff -r beeaa1ed1f47 -r 2ce69d6d5581 Admin/build
--- 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
 }
 
diff -r beeaa1ed1f47 -r 2ce69d6d5581 src/Pure/IsaMakefile
--- 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)
diff -r beeaa1ed1f47 -r 2ce69d6d5581 src/Pure/System/cygwin.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
 }
 
diff -r beeaa1ed1f47 -r 2ce69d6d5581 src/Pure/System/gui_setup.scala
--- /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)
+    }
+  }
+}
+
diff -r beeaa1ed1f47 -r 2ce69d6d5581 src/Pure/System/isabelle_system.scala
--- 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))
   }
diff -r beeaa1ed1f47 -r 2ce69d6d5581 src/Pure/System/platform.scala
--- /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
+      }
+    }
+  }
+}
+