# HG changeset patch
# User wenzelm
# Date 1378559433 -7200
# Node ID d12be8f6228500387d605a7440a986c5975ee9cc
# Parent e9a3390217b3e456df6a6abf6f9d93887427a485
Build_Dialog based on System_Dialog;
avoid hopping between threads;
diff -r e9a3390217b3 -r d12be8f62285 src/Pure/System/system_dialog.scala
--- a/src/Pure/System/system_dialog.scala Sat Sep 07 14:14:25 2013 +0200
+++ b/src/Pure/System/system_dialog.scala Sat Sep 07 15:10:33 2013 +0200
@@ -17,9 +17,6 @@
class System_Dialog extends Build.Progress
{
- val result = Future.promise[Int]
-
-
/* GUI state -- owned by Swing thread */
private var _title = "Isabelle"
@@ -46,11 +43,12 @@
}
}
+ private val result = Future.promise[Int]
+
private def conclude()
{
Swing_Thread.require()
require(_return_code.isDefined)
- require(!result.is_finished)
_window match {
case None =>
@@ -59,9 +57,12 @@
_window = None
}
- result.fulfill(_return_code.get)
+ try { result.fulfill(_return_code.get) }
+ catch { case ERROR(_) => }
}
+ def join(): Int = result.join
+
/* window */
@@ -164,7 +165,10 @@
def return_code(rc: Int): Unit =
Swing_Thread.later {
_return_code = Some(rc)
- _window.foreach(window => window.delay_exit.invoke)
+ _window match {
+ case None => conclude()
+ case Some(window) => window.delay_exit.invoke
+ }
}
override def echo(txt: String): Unit =
diff -r e9a3390217b3 -r d12be8f62285 src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala Sat Sep 07 14:14:25 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala Sat Sep 07 15:10:33 2013 +0200
@@ -18,7 +18,7 @@
{
/* command line entry point */
- def main(args: Array[String]) =
+ def main(args: Array[String])
{
GUI.init_laf()
try {
@@ -34,8 +34,9 @@
Isabelle_System.default_logic(logic,
if (logic_option != "") options.string(logic_option) else "")
- if (!dialog(options, system_mode, dirs, session, (rc: Int) => sys.exit(rc)))
- sys.exit(0)
+ val system_dialog = new System_Dialog
+ dialog(options, system_dialog, system_mode, dirs, session)
+ sys.exit(system_dialog.join)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
@@ -50,152 +51,34 @@
/* dialog */
- def dialog(options: Options, system_mode: Boolean, dirs: List[Path], session: String,
- continue: Int => Unit): Boolean =
+ def dialog(
+ options: Options,
+ system_dialog: System_Dialog,
+ system_mode: Boolean,
+ dirs: List[Path],
+ session: String)
{
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
+ more_dirs = more_dirs, sessions = List(session)) == 0)
+ system_dialog.return_code(0)
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,
- continue: Int => Unit): MainFrame = new MainFrame
- {
- iconImage = GUI.isabelle_image()
-
-
- /* GUI state */
-
- @volatile private var is_stopped = false
- private var return_code = 2
-
- def close(rc: Int) { visible = false; continue(rc) }
- override def closeOperation { close(return_code) }
-
-
- /* text */
-
- val text = new TextArea {
- font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
- editable = false
- columns = 50
- rows = 20
- }
-
- val scroll_text = new ScrollPane(text)
-
- val progress = new Build.Progress
- {
- override def echo(msg: String): Unit =
- Swing_Thread.later {
- text.append(msg + "\n")
- val vertical = scroll_text.peer.getVerticalScrollBar
- vertical.setValue(vertical.getMaximum)
- }
- override def theory(session: String, theory: String): Unit =
- echo(session + ": theory " + theory)
- override def stopped: Boolean = is_stopped
- }
-
-
- /* layout panel with dynamic actions */
+ system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
+ system_dialog.echo("Build started for Isabelle/" + session + " ...")
- val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
- val layout_panel = new BorderPanel
- layout_panel.layout(scroll_text) = BorderPanel.Position.Center
- layout_panel.layout(action_panel) = BorderPanel.Position.South
-
- contents = layout_panel
-
- def set_actions(cs: Component*)
- {
- action_panel.contents.clear
- action_panel.contents ++= cs
- layout_panel.revalidate
- layout_panel.repaint
- }
-
-
- /* actions */
-
- var do_auto_close = true
- def check_auto_close(): Unit =
- if (do_auto_close && return_code == 0) close(return_code)
-
- val auto_close = new CheckBox("Auto close") {
- reactions += {
- case ButtonClicked(_) => do_auto_close = this.selected
- check_auto_close()
- }
- }
- auto_close.selected = do_auto_close
- auto_close.tooltip = "Automatically close dialog when finished"
-
-
- val stop_button = new Button("Stop") {
- reactions += {
- case ButtonClicked(_) =>
- is_stopped = true
- set_actions(new Label("Stopping ..."))
- }
- }
-
- set_actions(stop_button, auto_close)
-
-
- /* exit */
-
- val delay_exit =
- Swing_Thread.delay_first(Time.seconds(1.0))
- {
- check_auto_close()
- val button =
- new Button(if (return_code == 0) "OK" else "Exit") {
- reactions += { case ButtonClicked(_) => close(return_code) }
- }
- set_actions(button)
- button.peer.getRootPane.setDefaultButton(button.peer)
- }
-
-
- /* main build */
-
- title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")"
- progress.echo("Build started for Isabelle/" + session + " ...")
-
- default_thread_pool.submit(() => {
val (out, rc) =
try {
("",
- Build.build(options = options, progress = progress,
+ Build.build(options = options, progress = system_dialog,
build_heap = true, more_dirs = more_dirs,
system_mode = system_mode, sessions = List(session)))
}
catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
- Swing_Thread.now {
- progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
- return_code = rc
- delay_exit.invoke()
- }
- })
+
+ system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+ system_dialog.return_code(rc)
+ }
}
}
diff -r e9a3390217b3 -r d12be8f62285 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala Sat Sep 07 14:14:25 2013 +0200
+++ b/src/Pure/Tools/main.scala Sat Sep 07 15:10:33 2013 +0200
@@ -14,14 +14,6 @@
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)
@@ -30,36 +22,100 @@
else body
}
- private def build_dialog(cont: Int => Unit)
+ def main(args: Array[String])
{
- try {
- GUI.init_laf()
- Isabelle_System.init()
+ val system_dialog = new System_Dialog
+
+ def exit_error(exn: Throwable): Nothing =
+ {
+ GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ system_dialog.return_code(2)
+ sys.exit(system_dialog.join)
+ }
+
+ def run
+ {
+ build
+ if (system_dialog.join == 0) start
+ }
+
+ def build
+ {
+ 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"))
+ val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+ if (mode == "none")
+ system_dialog.return_code(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"))
+ Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session)
+ }
+ }
+ catch { case exn: Throwable => exit_error(exn) }
+ }
- if (!Build_Dialog.dialog(options, system_mode, dirs, session, cont))
- cont(0)
- }
- }
- catch { case exn: Throwable => exit_error(exn) }
- }
+ def start
+ {
+ val do_start =
+ {
+ try {
+ /* settings directory */
+
+ val settings_dir = Path.explode("$JEDIT_SETTINGS")
+ Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
+
+ if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
+ File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
+ """""")
+ File.write(settings_dir + Path.explode("perspective.xml"),
+ """
+
+
+
+
+
+""")
+ }
- /* main entry point */
+ /* args */
+
+ val jedit_options =
+ Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
+
+ val jedit_settings =
+ Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
+
+ val more_args =
+ if (args.isEmpty)
+ Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+ else args
+
+
+ /* startup */
- def main(args: Array[String])
- {
- def start { start_jedit(ClassLoader.getSystemClassLoader, args) }
- def build { build_dialog(continue(start)) }
+ System.setProperty("jedit.home",
+ Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
+
+ System.setProperty("scala.home",
+ Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
+
+ val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit")
+ val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
+
+ () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
+ }
+ catch { case exn: Throwable => exit_error(exn) }
+ }
+ do_start()
+ }
if (Platform.is_windows) {
val init_isabelle_home =
@@ -90,74 +146,11 @@
init_isabelle_home match {
case Some(isabelle_home) =>
- Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(build)) }
- case None => build
+ Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(run)) }
+ case None => run
}
}
- else build
- }
-
-
- /* warm start of Isabelle/jEdit */
-
- def start_jedit(loader: ClassLoader, args: Array[String])
- {
- val start =
- {
- try {
- GUI.init_laf()
- Isabelle_System.init()
-
-
- /* settings directory */
-
- val settings_dir = Path.explode("$JEDIT_SETTINGS")
- Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
-
- if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
- File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
- """""")
- File.write(settings_dir + Path.explode("perspective.xml"),
- """
-
-
-
-
-
-""")
- }
-
-
- /* args */
-
- val jedit_options =
- Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
-
- val jedit_settings =
- Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
-
- val more_args =
- if (args.isEmpty)
- Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
- else args
-
-
- /* startup */
-
- System.setProperty("jedit.home",
- Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
-
- System.setProperty("scala.home",
- Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
-
- val jedit = loader.loadClass("org.gjt.sp.jedit.jEdit")
- val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
-
- () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
- }
- catch { case exn: Throwable => exit_error(exn) }
- }
- start()
+ else run
}
}