# 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 {