# HG changeset patch
# User wenzelm
# Date 1378405162 -7200
# Node ID 1c87e79bb83898318ff51129f27bbe3c6e13778e
# Parent d47a7cebe6b24188ac3cd9a170c0a9d0aaaf4681
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
standardized jdk location;
diff -r d47a7cebe6b2 -r 1c87e79bb838 Admin/Windows/Installer/sfx.txt
--- 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@!
diff -r d47a7cebe6b2 -r 1c87e79bb838 Admin/Windows/launch4j/isabelle.xml
--- 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 @@
%EXEDIR%\lib\classes\ext\scala-swing.jar
- %EXEDIR%\contrib\jdk-7u21\x86-cygwin\jdk1.7.0_21
+ %EXEDIR%\contrib\jdk\x86-cygwin
jdkOnly
- -Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin"
+ -Disabelle.home="%EXEDIR%"
isabelle.bmp
diff -r d47a7cebe6b2 -r 1c87e79bb838 src/Pure/System/cygwin_init.scala
--- 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")
}
diff -r d47a7cebe6b2 -r 1c87e79bb838 src/Pure/Tools/main.scala
--- 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
}
}