# HG changeset patch
# User wenzelm
# Date 1354721582 -3600
# Node ID e6c0720e4cefe6e9e1da7054da5ff87cc53d777e
# Parent  69efe72886e388af25866a9c182a53a702e9aedb
basic interaction with build process;

diff -r 69efe72886e3 -r e6c0720e4cef src/Pure/System/build_dialog.scala
--- a/src/Pure/System/build_dialog.scala	Wed Dec 05 16:31:58 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Wed Dec 05 16:33:02 2012 +0100
@@ -41,31 +41,31 @@
     title = "Isabelle session build"
 
 
-    /* controls */
+    /* GUI state */
 
     private var clean_build = false
-    private var system_build = false
-    private var verbose = false
+    private var system_mode = false
 
-    private val clean = new CheckBox("Clean build") {
+    private var is_started = false
+    private var is_stopped = false
+    private var return_code = 0
+
+
+    /* controls */
+
+    private val _clean_build = new CheckBox("Clean build") {
       reactions += { case ButtonClicked(_) => clean_build = this.selected }
     }
-    clean.selected = clean_build
-    clean.tooltip = "Delete outdated session images"
+    _clean_build.selected = clean_build
+    _clean_build.tooltip = "Delete outdated session images"
 
-    private val system = new CheckBox("System build") {
-      reactions += { case ButtonClicked(_) => system_build = this.selected }
+    private val _system_mode = new CheckBox("System build") {
+      reactions += { case ButtonClicked(_) => system_mode = this.selected }
     }
-    system.selected = system_build
-    system.tooltip = "Produce output in $ISABELLE_HOME instead of $ISABELLE_HOME_USER"
+    _system_mode.selected = system_mode
+    _system_mode.tooltip = "Produce output in $ISABELLE_HOME instead of $ISABELLE_HOME_USER"
 
-    private val verbose_mode = new CheckBox("Verbose mode") {
-      reactions += { case ButtonClicked(_) => verbose = this.selected }
-    }
-    verbose_mode.selected = verbose
-    verbose_mode.tooltip = "More output during build process"
-
-    val controls = new FlowPanel(FlowPanel.Alignment.Right)(clean, system, verbose_mode)
+    val controls = new FlowPanel(FlowPanel.Alignment.Right)(_clean_build, _system_mode)
 
 
     /* text */
@@ -76,25 +76,63 @@
       rows = 15
     }
 
+    val progress = new Build.Progress
+    {
+      override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
+      override def stopped: Boolean =
+        Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }
+    }
+
 
     /* actions */
 
-    val ok = new Button { text = "OK" }
-    val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
-
-    listenTo(ok)
-    reactions += {
-      case ButtonClicked(`ok`) => sys.exit(0)
+    val start = new Button("Start") {
+      reactions += { case ButtonClicked(_) =>
+        if (!is_started) {
+          progress.echo("Build started ...")
+          is_started = true
+          default_thread_pool.submit(() => {
+            val (out, rc) =
+              try {
+                ("",
+                  Build.build(progress, build_heap = true, verbose = true,
+                    clean_build = clean_build, system_mode = system_mode, sessions = List(session)))
+              }
+              catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
+            Swing_Thread.now {
+              if (rc != 0) {
+                progress.echo(out + "Return code: " + rc + "\n")
+                return_code = rc
+              }
+              is_started = false
+            }
+          })
+        }
+      }
     }
 
+    val stop = new Button("Stop") {
+      reactions += { case ButtonClicked(_) =>
+        progress.echo("Build stopped ...")
+        is_stopped = true
+      }
+    }
 
-    /* main panel */
+    val exit = new Button("Exit") {
+      reactions += { case ButtonClicked(_) => sys.exit(return_code) }
+    }
 
-    val panel = new BorderPanel
-    panel.layout(controls) = BorderPanel.Position.North
-    panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
-    panel.layout(ok_panel) = BorderPanel.Position.South
-    contents = panel
+    val actions = new FlowPanel(FlowPanel.Alignment.Center)(start, stop, exit)
+
+
+    /* layout panel */
+
+    val layout_panel = new BorderPanel
+    layout_panel.layout(controls) = BorderPanel.Position.North
+    layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
+    layout_panel.layout(actions) = BorderPanel.Position.South
+
+    contents = layout_panel
   }
 }