# HG changeset patch
# User wenzelm
# Date 1354713584 -3600
# Node ID 82f5aea343e74e608656ddce66ad030b7aa34c95
# Parent  ce2796981c0c6847c218c41e46972c7a09fb636b
basic wrapper for session build dialog;

diff -r ce2796981c0c -r 82f5aea343e7 lib/Tools/build_dialog
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/build_dialog	Wed Dec 05 14:19:44 2012 +0100
@@ -0,0 +1,63 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: build Isabelle session images via GUI dialog
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] SESSION"
+  echo
+  echo "  Options are:"
+  echo "    -d DIR       include session directory"
+  echo
+  echo "  Build Isabelle session images via GUI dialog."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+declare -a INCLUDE_DIRS=()
+
+while getopts "d:" OPT
+do
+  case "$OPT" in
+    d)
+      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 1 ] && usage
+
+SESSION="$1"; shift
+
+
+## main
+
+[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
+
+"$ISABELLE_TOOL" java isabelle.Build_Dialog "${INCLUDE_DIRS[@]}" $'\n' "$SESSION"
+
diff -r ce2796981c0c -r 82f5aea343e7 src/Pure/System/build_dialog.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/build_dialog.scala	Wed Dec 05 14:19:44 2012 +0100
@@ -0,0 +1,100 @@
+/*  Title:      Pure/System/build_dialog.scala
+    Author:     Makarius
+
+Dialog for session build process.
+*/
+
+package isabelle
+
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+  BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
+
+
+object Build_Dialog extends SwingApplication
+{
+  def startup(args: Array[String]) =
+  {
+    Platform.init_laf()
+
+    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 _ => error("Bad arguments:\n" + cat_lines(args))
+      }
+    }
+    catch {
+      case exn: Throwable =>
+        Library.error_dialog(null, "Isabelle build failure",
+          Library.scrollable_text(Exn.message(exn)))
+        sys.exit(2)
+    }
+  }
+
+
+  def build_dialog(include_dirs: List[Path], session: String): MainFrame = new MainFrame
+  {
+    title = "Isabelle session build"
+
+
+    /* controls */
+
+    private var clean_build = false
+    private var system_build = false
+    private var verbose = false
+
+    private val clean = new CheckBox("Clean build") {
+      reactions += { case ButtonClicked(_) => clean_build = this.selected }
+    }
+    clean.selected = clean_build
+    clean.tooltip = "Delete outdated session images"
+
+    private val system = new CheckBox("System build") {
+      reactions += { case ButtonClicked(_) => system_build = this.selected }
+    }
+    system.selected = system_build
+    system.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)
+
+
+    /* text */
+
+    val text = new TextArea {
+      editable = false
+      columns = 80
+      rows = 15
+    }
+
+
+    /* 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)
+    }
+
+
+    /* main panel */
+
+    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
+  }
+}
+
diff -r ce2796981c0c -r 82f5aea343e7 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Dec 05 14:13:47 2012 +0100
+++ b/src/Pure/build-jars	Wed Dec 05 14:19:44 2012 +0100
@@ -39,6 +39,7 @@
   PIDE/xml.scala
   PIDE/yxml.scala
   System/build.scala
+  System/build_dialog.scala
   System/color_value.scala
   System/command_line.scala
   System/event_bus.scala