avoid startup within GUI thread -- it is only required later for dialog;
tuned signature;
--- 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[@]}"
--- 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))
}
--- 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) }