--- 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)
+ }
}
}