# HG changeset patch # User wenzelm # Date 1354725523 -3600 # Node ID d5dbb63df0c770085072462f4695ef6f59f9a41c # Parent 622002c702ad519cd6d4f2b6a0ce6a54aa36f83a check for existing image (even if outdated); removed conflicting "clean" option; diff -r 622002c702ad -r d5dbb63df0c7 lib/Tools/build_dialog --- a/lib/Tools/build_dialog Wed Dec 05 17:05:25 2012 +0100 +++ b/lib/Tools/build_dialog Wed Dec 05 17:38:43 2012 +0100 @@ -15,7 +15,7 @@ echo "Usage: isabelle $PRG [OPTIONS] SESSION" echo echo " Options are:" - echo " -c clean build" + echo " -C check for existing image" echo " -d DIR include session directory" echo " -s system build mode: produce output in ISABELLE_HOME" echo @@ -33,15 +33,15 @@ ## process command line -CLEAN_BUILD=false +CHECK_EXISTING=false declare -a INCLUDE_DIRS=() SYSTEM_MODE=false -while getopts "cd:s" OPT +while getopts "Cd:s" OPT do case "$OPT" in - c) - CLEAN_BUILD="true" + C) + CHECK_EXISTING="true" ;; d) INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" @@ -65,10 +65,27 @@ SESSION="$1"; shift -## main +## existing image -[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } +EXISTING=false +if [ "$CHECK_EXISTING" = true ]; then + declare -a ISABELLE_PATHS=() + splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}") -"$ISABELLE_TOOL" java isabelle.Build_Dialog \ - "$CLEAN_BUILD" "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}" + for DIR in "${ISABELLE_PATHS[@]}" + do + FILE="$DIR/$ML_IDENTIFIER/$SESSION" + [ -f "$FILE" ] && EXISTING=true + done +fi + +## build + +if [ "$EXISTING" = false ]; then + [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } + + "$ISABELLE_TOOL" java isabelle.Build_Dialog \ + "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}" +fi + diff -r 622002c702ad -r d5dbb63df0c7 src/Pure/System/build_dialog.scala --- a/src/Pure/System/build_dialog.scala Wed Dec 05 17:05:25 2012 +0100 +++ b/src/Pure/System/build_dialog.scala Wed Dec 05 17:38:43 2012 +0100 @@ -21,11 +21,9 @@ try { args.toList match { 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) + val top = build_dialog(system_mode, include_dirs.map(Path.explode), session) top.pack() top.visible = true case _ => error("Bad arguments:\n" + cat_lines(args)) @@ -41,7 +39,6 @@ def build_dialog( - clean_build: Boolean, system_mode: Boolean, include_dirs: List[Path], session: String): MainFrame = new MainFrame @@ -98,7 +95,7 @@ try { ("", Build.build(progress, build_heap = true, - clean_build = clean_build, system_mode = system_mode, sessions = List(session))) + system_mode = system_mode, sessions = List(session))) } catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } Swing_Thread.now {