# 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 } }