# HG changeset patch
# User wenzelm
# Date 1354723525 -3600
# Node ID 622002c702ad519cd6d4f2b6a0ce6a54aa36f83a
# Parent  e6c0720e4cefe6e9e1da7054da5ff87cc53d777e
more elementary dialog, with less interaction;

diff -r e6c0720e4cef -r 622002c702ad lib/Tools/build_dialog
--- a/lib/Tools/build_dialog	Wed Dec 05 16:33:02 2012 +0100
+++ b/lib/Tools/build_dialog	Wed Dec 05 17:05:25 2012 +0100
@@ -15,9 +15,11 @@
   echo "Usage: isabelle $PRG [OPTIONS] SESSION"
   echo
   echo "  Options are:"
+  echo "    -c           clean build"
   echo "    -d DIR       include session directory"
+  echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo
-  echo "  Build Isabelle session images via GUI dialog."
+  echo "  Build Isabelle session image via GUI dialog."
   echo
   exit 1
 }
@@ -31,14 +33,22 @@
 
 ## process command line
 
+CLEAN_BUILD=false
 declare -a INCLUDE_DIRS=()
+SYSTEM_MODE=false
 
-while getopts "d:" OPT
+while getopts "cd:s" OPT
 do
   case "$OPT" in
+    c)
+      CLEAN_BUILD="true"
+      ;;
     d)
       INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
       ;;
+    s)
+      SYSTEM_MODE="true"
+      ;;
     \?)
       usage
       ;;
@@ -59,5 +69,6 @@
 
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
-"$ISABELLE_TOOL" java isabelle.Build_Dialog "${INCLUDE_DIRS[@]}" $'\n' "$SESSION"
+"$ISABELLE_TOOL" java isabelle.Build_Dialog \
+  "$CLEAN_BUILD" "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}"
 
diff -r e6c0720e4cef -r 622002c702ad src/Pure/System/build_dialog.scala
--- a/src/Pure/System/build_dialog.scala	Wed Dec 05 16:33:02 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Wed Dec 05 17:05:25 2012 +0100
@@ -20,10 +20,14 @@
 
     try {
       args.toList match {
-        case Command_Line.Chunks(include_dirs, List(session)) =>
-          val top = build_dialog(include_dirs.map(Path.explode), session)
-          top.pack()
-          top.visible = true
+        case
+          Properties.Value.Boolean(clean_build) ::
+          Properties.Value.Boolean(system_mode) ::
+          session :: include_dirs =>
+            val top =
+              build_dialog(clean_build, system_mode, include_dirs.map(Path.explode), session)
+            top.pack()
+            top.visible = true
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }
@@ -36,44 +40,27 @@
   }
 
 
-  def build_dialog(include_dirs: List[Path], session: String): MainFrame = new MainFrame
+  def build_dialog(
+    clean_build: Boolean,
+    system_mode: Boolean,
+    include_dirs: List[Path],
+    session: String): MainFrame = new MainFrame
   {
-    title = "Isabelle session build"
+    title = "Isabelle build"
 
 
     /* GUI state */
 
-    private var clean_build = false
-    private var system_mode = false
-
-    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_build.selected = clean_build
-    _clean_build.tooltip = "Delete outdated session images"
-
-    private val _system_mode = new CheckBox("System build") {
-      reactions += { case ButtonClicked(_) => system_mode = this.selected }
-    }
-    _system_mode.selected = system_mode
-    _system_mode.tooltip = "Produce output in $ISABELLE_HOME instead of $ISABELLE_HOME_USER"
-
-    val controls = new FlowPanel(FlowPanel.Alignment.Right)(_clean_build, _system_mode)
-
-
     /* text */
 
     val text = new TextArea {
       editable = false
-      columns = 80
-      rows = 15
+      columns = 40
+      rows = 10
     }
 
     val progress = new Build.Progress
@@ -86,53 +73,42 @@
 
     /* actions */
 
-    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 cancel = new Button("Cancel") {
+      reactions += { case ButtonClicked(_) => is_stopped = true }
     }
 
-    val stop = new Button("Stop") {
-      reactions += { case ButtonClicked(_) =>
-        progress.echo("Build stopped ...")
-        is_stopped = true
-      }
-    }
-
-    val exit = new Button("Exit") {
-      reactions += { case ButtonClicked(_) => sys.exit(return_code) }
-    }
-
-    val actions = new FlowPanel(FlowPanel.Alignment.Center)(start, stop, exit)
+    val actions = new FlowPanel(FlowPanel.Alignment.Center)(cancel)
 
 
     /* 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
+
+
+    /* main build */
+
+    progress.echo("Build started ...")
+
+    default_thread_pool.submit(() => {
+      val (out, rc) =
+        try {
+          ("",
+            Build.build(progress, build_heap = 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) {
+          Library.error_dialog(this.peer, "Isabelle build failure",
+            Library.scrollable_text(out + "Return code: " + rc + "\n"))
+        }
+        sys.exit(rc)
+      }
+    })
   }
 }