main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
standardized jdk location;

--- a/Admin/Windows/Installer/sfx.txt	Thu Sep 05 16:39:01 2013 +0200
+++ b/Admin/Windows/Installer/sfx.txt	Thu Sep 05 20:19:22 2013 +0200
@@ -5,5 +5,5 @@
 ExtractPathText="Target directory"
 ExtractTitle="Unpacking {ISABELLE_NAME} ..."
 Shortcut="Du,{%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe},{},{},{},{{ISABELLE_NAME}},{%%T\{ISABELLE_NAME}}"
-RunProgram="\"%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe\" -i"
+RunProgram="\"%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe\""
 ;!@InstallEnd@!

--- a/Admin/Windows/launch4j/isabelle.xml	Thu Sep 05 16:39:01 2013 +0200
+++ b/Admin/Windows/launch4j/isabelle.xml	Thu Sep 05 20:19:22 2013 +0200
@@ -20,11 +20,11 @@
     <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
   </classPath>
   <jre>
-    <path>%EXEDIR%\contrib\jdk-7u21\x86-cygwin\jdk1.7.0_21</path>
+    <path>%EXEDIR%\contrib\jdk\x86-cygwin</path>
     <minVersion></minVersion>
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
-    <opt>-Disabelle.home=&quot;%EXEDIR%&quot; -Dcygwin.root=&quot;%EXEDIR%\\contrib\\cygwin&quot;</opt>
+    <opt>-Disabelle.home=&quot;%EXEDIR%&quot;</opt>
   </jre>
   <splash>
     <file>isabelle.bmp</file>

--- a/src/Pure/System/cygwin_init.scala	Thu Sep 05 16:39:01 2013 +0200
+++ b/src/Pure/System/cygwin_init.scala	Thu Sep 05 20:19:22 2013 +0200
@@ -7,7 +7,6 @@
 package isabelle
 
 
-import java.lang.System
 import java.io.{File => JFile, BufferedReader, InputStreamReader}
 import java.nio.file.{Paths, Files}
 import java.awt.{GraphicsEnvironment, Point, Font}
@@ -21,33 +20,9 @@
 
 object Cygwin_Init
 {
-  /* command-line entry point */
-
-  def main(args: Array[String]) =
-  {
-    GUI.init_laf()
-    try {
-      require(Platform.is_windows)
-
-      val isabelle_home = System.getProperty("isabelle.home")
-      if (isabelle_home == null || isabelle_home == "")
-        error("Unknown Isabelle home directory")
-      if (!(new JFile(isabelle_home)).isDirectory)
-        error("Bad Isabelle home directory: " + quote(isabelle_home))
+  /* main GUI entry point */
 
-      Swing_Thread.later { main_frame(isabelle_home) }
-    }
-    catch {
-      case exn: Throwable =>
-        GUI.error_dialog(null, "Isabelle init failure", GUI.scrollable_text(Exn.message(exn)))
-        sys.exit(2)
-    }
-  }
-
-
-  /* main window */
-
-  private def main_frame(isabelle_home: String) = new MainFrame
+  def main_frame(isabelle_home: String, start: => Unit) = new MainFrame
   {
     title = "Isabelle system initialization"
     iconImage = new ImageIcon(isabelle_home + "\\lib\\logo\\isabelle.gif").getImage
@@ -73,7 +48,14 @@
     /* exit button */
 
     var _return_code: Option[Int] = None
-    def maybe_exit(): Unit = _return_code.foreach(sys.exit(_))
+    def maybe_exit()
+    {
+      _return_code match {
+        case None =>
+        case Some(0) => start
+        case Some(rc) => sys.exit(rc)
+      }
+    }
 
     def return_code(rc: Int): Unit =
       Swing_Thread.later {
@@ -102,7 +84,7 @@
 
     default_thread_pool.submit(() =>
       try {
-        init(isabelle_home, echo)
+        init_filesystem(isabelle_home, echo)
         return_code(0)
       }
       catch {
@@ -116,13 +98,8 @@
 
   /* init Cygwin file-system */
 
-  private def init(isabelle_home: String, echo: String => Unit)
+  private def init_filesystem(isabelle_home: String, echo: String => Unit)
   {
-    val cygwin_root = isabelle_home + "\\contrib\\cygwin"
-
-    if (!(new JFile(cygwin_root)).isDirectory)
-      error("Bad Isabelle Cygwin directory: " + quote(cygwin_root))
-
     def execute(args: String*): Int =
     {
       val cwd = new JFile(isabelle_home)
@@ -148,7 +125,7 @@
     echo("symlinks ...")
     val symlinks =
     {
-      val path = (new JFile(cygwin_root, "isabelle\\symlinks")).toPath
+      val path = (new JFile("contrib\\cygwin\\isabelle\\symlinks")).toPath
       Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
     }
     @tailrec def recover_symlinks(list: List[String]): Unit =
@@ -171,13 +148,12 @@
     recover_symlinks(symlinks)
 
     echo("rebaseall ...")
-    execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+    execute("contrib\\cygwin\\bin\\dash.exe", "/isabelle/rebaseall")
 
     echo("postinstall ...")
-    execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
+    execute("contrib\\cygwin\\bin\\bash.exe", "/isabelle/postinstall")
 
     echo("init ...")
-    System.setProperty("cygwin.root", cygwin_root)
     Isabelle_System.init()
     echo("OK")
   }

--- a/src/Pure/Tools/main.scala	Thu Sep 05 16:39:01 2013 +0200
+++ b/src/Pure/Tools/main.scala	Thu Sep 05 20:19:22 2013 +0200
@@ -1,37 +1,72 @@
 /*  Title:      Pure/Tools/main.scala
     Author:     Makarius
 
-Default Isabelle application wrapper.
+Main Isabelle application entry point.
 */
 
 package isabelle
 
-import scala.swing.TextArea
+
+import java.lang.System
+import java.io.{File => JFile}
 
 
 object Main
 {
   def main(args: Array[String])
   {
-    args.toList match {
-      case "-i" :: rest =>
-        if (Platform.is_windows) Cygwin_Init.main(rest.toArray)
+    def start: Unit =
+    {
+      val (out, rc) =
+        try {
+          GUI.init_laf()
+          Isabelle_System.init()
+          Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*)
+        }
+        catch { case exn: Throwable => (Exn.message(exn), 2) }
+
+      if (rc != 0)
+        GUI.dialog(null, "Isabelle", "Isabelle output",
+          GUI.scrollable_text(out + "\nReturn code: " + rc))
+
+      sys.exit(rc)
+    }
+
+    if (Platform.is_windows) {
+      val init_isabelle_home =
+        try {
+          GUI.init_laf()
+
+          val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS")
+          val isabelle_home = System.getProperty("isabelle.home")
 
-      case _ =>
-        val (out, rc) =
-          try {
-            GUI.init_laf()
-            Isabelle_System.init()
-            Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*)
+          if (isabelle_home0 != null && isabelle_home0 != "") None
+          else {
+            if (isabelle_home == null || isabelle_home == "")
+              error("Unknown Isabelle home directory")
+            if (!(new JFile(isabelle_home)).isDirectory)
+              error("Bad Isabelle home directory: " + quote(isabelle_home))
+
+            val uninitialized_file =
+              new JFile(isabelle_home, "contrib\\cygwin\\isabelle\\uninitialized")
+            val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+
+            if (uninitialized) Some(isabelle_home) else None
           }
-          catch { case exn: Throwable => (Exn.message(exn), 2) }
-
-        if (rc != 0)
-          GUI.dialog(null, "Isabelle", "Isabelle output",
-            GUI.scrollable_text(out + "\nReturn code: " + rc))
-
-        sys.exit(rc)
+        }
+        catch {
+          case exn: Throwable =>
+            GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+            sys.exit(2)
+        }
+      init_isabelle_home match {
+        case Some(isabelle_home) =>
+          GUI.dialog(null, "Isabelle", GUI.scrollable_text("OK"))
+          Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, start) }
+        case None => start
+      }
     }
+    else start
   }
 }