--- a/src/Pure/System/cygwin_init.scala Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Pure/System/cygwin_init.scala Sat Sep 07 00:02:19 2013 +0200
@@ -22,7 +22,7 @@
{
/* main GUI entry point */
- def main_frame(isabelle_home: String, start: => Unit) = new MainFrame
+ def main_frame(isabelle_home: String, continue: Int => Unit) = new MainFrame
{
title = "Isabelle system initialization"
iconImage = new ImageIcon(isabelle_home + "\\lib\\logo\\isabelle.gif").getImage
@@ -52,11 +52,9 @@
{
_return_code match {
case None =>
- case Some(0) =>
+ case Some(rc) =>
visible = false
- Simple_Thread.fork("Isabelle") { start }
- case Some(rc) =>
- sys.exit(rc)
+ continue(rc)
}
}
--- a/src/Pure/Tools/build_dialog.scala Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala Sat Sep 07 00:02:19 2013 +0200
@@ -16,6 +16,8 @@
object Build_Dialog
{
+ /* command line entry point */
+
def main(args: Array[String]) =
{
GUI.init_laf()
@@ -26,26 +28,15 @@
logic ::
Properties.Value.Boolean(system_mode) ::
include_dirs =>
- val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
-
val options = Options.init()
+ val dirs = include_dirs.map(Path.explode(_))
val session =
Isabelle_System.default_logic(logic,
if (logic_option != "") options.string(logic_option) else "")
- if (Build.build(options = options, build_heap = true, no_build = true,
- more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
- else
- Swing_Thread.later {
- val top = build_dialog(options, system_mode, more_dirs, session)
- top.pack()
+ if (!dialog(options, system_mode, dirs, session, (rc: Int) => sys.exit(rc)))
+ sys.exit(0)
- val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
- top.location =
- new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
-
- top.visible = true
- }
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
@@ -57,11 +48,36 @@
}
+ /* dialog */
+
+ def dialog(options: Options, system_mode: Boolean, dirs: List[Path], session: String,
+ continue: Int => Unit): Boolean =
+ {
+ val more_dirs = dirs.map((false, _))
+
+ if (Build.build(options = options, build_heap = true, no_build = true,
+ more_dirs = more_dirs, sessions = List(session)) == 0) false
+ else {
+ Swing_Thread.later {
+ val top = build_dialog(options, system_mode, more_dirs, session, continue)
+ top.pack()
+
+ val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
+ top.location =
+ new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
+
+ top.visible = true
+ }
+ true
+ }
+ }
+
def build_dialog(
options: Options,
system_mode: Boolean,
more_dirs: List[(Boolean, Path)],
- session: String): MainFrame = new MainFrame
+ session: String,
+ continue: Int => Unit): MainFrame = new MainFrame
{
iconImage = GUI.isabelle_image()
@@ -71,7 +87,8 @@
@volatile private var is_stopped = false
private var return_code = 2
- override def closeOperation { sys.exit(return_code) }
+ def close(rc: Int) { visible = false; continue(rc) }
+ override def closeOperation { close(return_code) }
/* text */
@@ -120,7 +137,8 @@
/* actions */
var do_auto_close = true
- def check_auto_close(): Unit = if (do_auto_close && return_code == 0) sys.exit(return_code)
+ def check_auto_close(): Unit =
+ if (do_auto_close && return_code == 0) close(return_code)
val auto_close = new CheckBox("Auto close") {
reactions += {
@@ -151,7 +169,7 @@
check_auto_close()
val button =
new Button(if (return_code == 0) "OK" else "Exit") {
- reactions += { case ButtonClicked(_) => sys.exit(return_code) }
+ reactions += { case ButtonClicked(_) => close(return_code) }
}
set_actions(button)
button.peer.getRootPane.setDefaultButton(button.peer)
--- a/src/Pure/Tools/main.scala Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Pure/Tools/main.scala Sat Sep 07 00:02:19 2013 +0200
@@ -7,24 +7,59 @@
package isabelle
+import javax.swing.SwingUtilities
import java.lang.{System, ClassLoader}
import java.io.{File => JFile}
object Main
{
+ /* auxiliary dialogs */
+
private def exit_error(exn: Throwable): Nothing =
{
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
sys.exit(2)
}
+ private def continue(body: => Unit)(rc: Int)
+ {
+ if (rc != 0) sys.exit(rc)
+ else if (SwingUtilities.isEventDispatchThread())
+ Simple_Thread.fork("Isabelle") { body }
+ else body
+ }
- /** main entry point **/
+ private def build_dialog(cont: Int => Unit)
+ {
+ try {
+ GUI.init_laf()
+ Isabelle_System.init()
+
+ val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+ if (mode == "none") cont(0)
+ else {
+ val system_mode = mode == "" || mode == "system"
+ val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+ val options = Options.init()
+ val session = Isabelle_System.default_logic(
+ Isabelle_System.getenv("JEDIT_LOGIC"),
+ options.string("jedit_logic"))
+
+ if (!Build_Dialog.dialog(options, system_mode, dirs, session, cont))
+ cont(0)
+ }
+ }
+ catch { case exn: Throwable => exit_error(exn) }
+ }
+
+
+ /* main entry point */
def main(args: Array[String])
{
def start { start_jedit(ClassLoader.getSystemClassLoader, args) }
+ def build { build_dialog(continue(start)) }
if (Platform.is_windows) {
val init_isabelle_home =
@@ -55,16 +90,15 @@
init_isabelle_home match {
case Some(isabelle_home) =>
- Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, start) }
- case None => start
+ Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(build)) }
+ case None => build
}
}
- else start
+ else build
}
-
- /** warm start of Isabelle/jEdit **/
+ /* warm start of Isabelle/jEdit */
def start_jedit(loader: ClassLoader, args: Array[String])
{
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Sep 07 00:02:19 2013 +0200
@@ -108,14 +108,12 @@
# options
-declare -a BUILD_DIALOG_OPTIONS=(-L jedit_logic)
-
BUILD_ONLY=false
BUILD_JARS="jars"
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
-NO_BUILD="false"
+JEDIT_BUILD_MODE="normal"
function getoptions()
{
@@ -135,8 +133,6 @@
else
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
fi
- BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-d"
- BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
;;
f)
BUILD_JARS="jars_fresh"
@@ -145,8 +141,6 @@
ARGS["${#ARGS[@]}"]="$OPTARG"
;;
l)
- BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-l"
- BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
JEDIT_LOGIC="$OPTARG"
;;
m)
@@ -157,10 +151,10 @@
fi
;;
n)
- NO_BUILD="true"
+ JEDIT_BUILD_MODE="none"
;;
s)
- BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s"
+ JEDIT_BUILD_MODE="system"
;;
\?)
usage
@@ -320,13 +314,7 @@
## main
if [ "$BUILD_ONLY" = false ]; then
- if [ "$NO_BUILD" = false ]; then
- "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
- RC="$?"
- [ "$RC" = 0 ] || exit "$RC"
- fi
-
- export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
+ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
-classpath "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" isabelle.Main "${ARGS[@]}"