diff -r be0f7f4f9e12 -r 4345173ee386 src/Pure/System/cygwin.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/cygwin.scala	Mon Jun 08 00:20:43 2009 +0200
@@ -0,0 +1,84 @@
+/*  Title:      Pure/System/cygwin.scala
+    Author:     Makarius
+
+Accessing the Cygwin installation.
+*/
+
+package isabelle
+
+import java.lang.reflect.Method
+
+
+object Cygwin
+{
+  /* registry access */
+
+  // Some black magic involving private WindowsPreferences from Sun, cf.
+  // http://www.docjar.com/html/api/java/util/prefs/WindowsPreferences.java.html
+
+  private val WindowsPreferences = Class.forName("java.util.prefs.WindowsPreferences")
+
+  private val HKEY_CURRENT_USER = 0x80000001
+  private val HKEY_LOCAL_MACHINE = 0x80000002
+  private val KEY_READ = 0x20019
+  private val NATIVE_HANDLE = 0
+  private val ERROR_CODE = 1
+
+  private def C_string(s: String): Array[Byte] =
+    (s + "\0").getBytes("US-ASCII")
+
+  private def J_string(bs: Array[Byte]): String =
+    new String(bs, 0, bs.length - 1, "US-ASCII")
+
+  private val INT = Integer.TYPE
+  private val BYTES = (new Array[Byte](0)).getClass
+
+  private def open_key(handle: Int, subkey: Array[Byte], mask: Int): Array[Int] =
+  {
+    val m = WindowsPreferences.getDeclaredMethod("WindowsRegOpenKey", INT, BYTES, INT)
+    m.setAccessible(true)
+    m.invoke(null, handle.asInstanceOf[Object], subkey.asInstanceOf[Object],
+      mask.asInstanceOf[Object]).asInstanceOf[Array[Int]]
+  }
+
+  private def close_key(handle: Int): Int =
+  {
+    val m = WindowsPreferences.getDeclaredMethod("WindowsRegCloseKey", INT)
+    m.setAccessible(true)
+    m.invoke(null, handle.asInstanceOf[Object]).asInstanceOf[Int]
+  }
+
+  private def query(handle: Int, name: Array[Byte]) =
+  {
+    val m = WindowsPreferences.getDeclaredMethod("WindowsRegQueryValueEx", INT, BYTES)
+    m.setAccessible(true)
+    m.invoke(null, handle.asInstanceOf[Object], name.asInstanceOf[Object]).
+      asInstanceOf[Array[Byte]]
+  }
+
+  def query_registry(sys: Boolean, path: String, name: String): Option[String] =
+  {
+    val handle = if (sys) HKEY_LOCAL_MACHINE else HKEY_CURRENT_USER
+    val result = open_key(handle, C_string(path), KEY_READ)
+    if (result(ERROR_CODE) != 0) None
+    else {
+      val res = query(result(NATIVE_HANDLE), C_string(name))
+      if (res == null) None
+      else Some(J_string(res))
+    }
+  }
+
+  def query_registry(path: String, name: String): Option[String] =
+    query_registry(false, path, name) orElse
+      query_registry(true, path, name)
+
+
+  /* Cygwin installation */
+
+  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")
+
+}
+