some more Cygwin checks;

--- a/src/Pure/System/cygwin.scala	Sun Jun 28 14:27:42 2009 +0200
+++ b/src/Pure/System/cygwin.scala	Sun Jun 28 15:39:51 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
 }
 

--- a/src/Pure/System/isabelle_system.scala	Sun Jun 28 14:27:42 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Jun 28 15:39:51 2009 +0200
@@ -63,8 +63,8 @@
   private val (platform_root, drive_prefix, shell_prefix) =
   {
     if (Platform.is_windows) {
-      val root = Cygwin.root() getOrElse "C:\\cygwin"
-      val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
+      val (drive, root) = Cygwin.config()
+      if (!Cygwin.check(root)) error("Bad Cygwin installation: " + root)
       val shell = List(root + "\\bin\\bash", "-l")
       (root, drive, shell)
     }