# HG changeset patch
# User wenzelm
# Date 1354821974 -3600
# Node ID 898cac1dad5eb2d4f49f5d74900cc874a68375ed
# Parent  87868964733c99e90ea5d9e8f8694ccdd029b025
avoid startup within GUI thread -- it is only required later for dialog;
tuned signature;

diff -r 87868964733c -r 898cac1dad5e lib/Tools/build_dialog
--- a/lib/Tools/build_dialog	Thu Dec 06 17:59:37 2012 +0100
+++ b/lib/Tools/build_dialog	Thu Dec 06 20:26:14 2012 +0100
@@ -12,7 +12,7 @@
 function usage()
 {
   echo
-  echo "Usage: isabelle $PRG [OPTIONS] SESSION"
+  echo "Usage: isabelle $PRG [OPTIONS] LOGIC"
   echo
   echo "  Options are:"
   echo "    -C           check for existing image"
@@ -20,7 +20,7 @@
   echo "    -d DIR       include session directory"
   echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo
-  echo "  Build Isabelle session image via GUI dialog."
+  echo "  Build Isabelle session image LOGIC via GUI dialog."
   echo
   exit 1
 }
@@ -67,7 +67,7 @@
 
 [ "$#" -ne 1 ] && usage
 
-SESSION="$1"; shift
+LOGIC="$1"; shift
 
 
 ## main
@@ -75,5 +75,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 "$ISABELLE_TOOL" java isabelle.Build_Dialog \
-  "$CHECK_EXISTING" "$LOGIC_OPTION" "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}"
+  "$CHECK_EXISTING" "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}"
 
diff -r 87868964733c -r 898cac1dad5e src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Dec 06 17:59:37 2012 +0100
+++ b/src/Pure/System/build.scala	Thu Dec 06 20:26:14 2012 +0100
@@ -399,7 +399,7 @@
 
   def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
   {
-    val options = Options.init
+    val options = Options.init()
     val (_, tree) =
       find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
     dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
@@ -550,6 +550,7 @@
 
   def build(
     progress: Build.Progress,
+    options: Options,
     requirements: Boolean = false,
     all_sessions: Boolean = false,
     build_heap: Boolean = false,
@@ -559,12 +560,10 @@
     max_jobs: Int = 1,
     list_files: Boolean = false,
     no_build: Boolean = false,
-    build_options: List[String] = Nil,
     system_mode: Boolean = false,
     verbose: Boolean = false,
     sessions: List[String] = Nil): Int =
   {
-    val options = (Options.init() /: build_options)(_ + _)
     val full_tree = find_sessions(options, more_dirs)
     val (selected, selected_tree) =
       full_tree.selection(requirements, all_sessions, session_groups, sessions)
@@ -735,11 +734,12 @@
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
+            val options = (Options.init() /: build_options)(_ + _)
             val dirs =
               select_dirs.map(d => (true, Path.explode(d))) :::
               include_dirs.map(d => (false, Path.explode(d)))
-            build(Build.Console_Progress, requirements, all_sessions, build_heap, clean_build,
-              dirs, session_groups, max_jobs, list_files, no_build, build_options, system_mode,
+            build(Build.Console_Progress, options, requirements, all_sessions, build_heap,
+              clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode,
               verbose, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
diff -r 87868964733c -r 898cac1dad5e src/Pure/System/build_dialog.scala
--- a/src/Pure/System/build_dialog.scala	Thu Dec 06 17:59:37 2012 +0100
+++ b/src/Pure/System/build_dialog.scala	Thu Dec 06 20:26:14 2012 +0100
@@ -14,24 +14,24 @@
 import scala.swing.event.ButtonClicked
 
 
-object Build_Dialog extends SwingApplication
+object Build_Dialog
 {
-  // FIXME avoid startup via GUI thread!?
-  def startup(args: Array[String]) =
+  def main(args: Array[String]) =
   {
-    Platform.init_laf()
-
     try {
       args.toList match {
         case
           Properties.Value.Boolean(check_existing) ::
           logic_option ::
           Properties.Value.Boolean(system_mode) ::
-          session_arg ::
+          logic ::
           include_dirs =>
+            val dirs = include_dirs.map(Path.explode)
+
+            val options = Options.init()
             val session =
-              Isabelle_System.default_logic(session_arg,
-                if (logic_option != "") Options.init().string(logic_option) else "")
+              Isabelle_System.default_logic(logic,
+                if (logic_option != "") options.string(logic_option) else "")
 
             val no_dialog =  // FIXME full up-to-date test!?
               check_existing &&
@@ -39,13 +39,18 @@
                   (dir + Path.basic(session)).is_file)
 
             if (no_dialog) sys.exit(0)
-            else {
-              val center = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
-              val top = build_dialog(system_mode, include_dirs.map(Path.explode), session)
-              top.pack()
-              top.location = new Point(center.x - top.size.width / 2, center.y - top.size.height / 2)
-              top.visible = true
-            }
+            else
+              Swing_Thread.later {
+                Platform.init_laf()
+
+                val top = build_dialog(options, system_mode, dirs, session)
+                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
+              }
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }
@@ -59,8 +64,9 @@
 
 
   def build_dialog(
+    options: Options,
     system_mode: Boolean,
-    include_dirs: List[Path],
+    dirs: List[Path],
     session: String): MainFrame = new MainFrame
   {
     /* GUI state */
@@ -120,7 +126,7 @@
       val (out, rc) =
         try {
           ("",
-            Build.build(progress, build_heap = true,
+            Build.build(progress, options, build_heap = true, more_dirs = dirs.map((false, _)),
               system_mode = system_mode, sessions = List(session)))
         }
         catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }