# HG changeset patch
# User wenzelm
# Date 1343590846 -7200
# Node ID a125b8040ada37a96cf11f304dca9e9f408e6c30
# Parent  38e225bd53e48b7cd227f341a5a2febcc5eee6b9
added build option -f;

diff -r 38e225bd53e4 -r a125b8040ada doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Sat Jul 28 22:01:21 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Sun Jul 29 21:40:46 2012 +0200
@@ -168,6 +168,7 @@
     -a           select all sessions
     -b           build heap images
     -d DIR       include session directory with ROOT file
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -n           no build -- test dependencies only
@@ -221,6 +222,9 @@
   saved for inner nodes of the hierarchy of sessions, as required for
   other sessions to continue later on.
 
+  \medskip Option @{verbatim "-f"} ensures a fresh build, even if all
+  results are up-to-date wrt.\ the current set of sources.
+
   \medskip Option @{verbatim "-j"} specifies the maximum number of
   parallel build jobs (prover processes).  Note that each process is
   subject to a separate limit of parallel threads, cf.\ system option
diff -r 38e225bd53e4 -r a125b8040ada doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Sat Jul 28 22:01:21 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Sun Jul 29 21:40:46 2012 +0200
@@ -278,6 +278,7 @@
     -a           select all sessions
     -b           build heap images
     -d DIR       include session directory with ROOT file
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -n           no build -- test dependencies only
@@ -327,6 +328,9 @@
   saved for inner nodes of the hierarchy of sessions, as required for
   other sessions to continue later on.
 
+  \medskip Option \verb|-f| ensures a fresh build, even if all
+  results are up-to-date wrt.\ the current set of sources.
+
   \medskip Option \verb|-j| specifies the maximum number of
   parallel build jobs (prover processes).  Note that each process is
   subject to a separate limit of parallel threads, cf.\ system option
diff -r 38e225bd53e4 -r a125b8040ada lib/Tools/build
--- a/lib/Tools/build	Sat Jul 28 22:01:21 2012 +0200
+++ b/lib/Tools/build	Sun Jul 29 21:40:46 2012 +0200
@@ -29,6 +29,7 @@
   echo "    -a           select all sessions"
   echo "    -b           build heap images"
   echo "    -d DIR       include session directory with ROOT file"
+  echo "    -f           fresh build"
   echo "    -g NAME      select session group NAME"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
   echo "    -n           no build -- test dependencies only"
@@ -59,6 +60,7 @@
 ALL_SESSIONS=false
 BUILD_HEAP=false
 declare -a MORE_DIRS=()
+FRESH_BUILD=false
 declare -a SESSION_GROUPS=()
 MAX_JOBS=1
 NO_BUILD=false
@@ -66,7 +68,7 @@
 SYSTEM_MODE=false
 VERBOSE=false
 
-while getopts "abd:g:j:no:sv" OPT
+while getopts "abd:fg:j:no:sv" OPT
 do
   case "$OPT" in
     a)
@@ -78,6 +80,9 @@
     d)
       MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
       ;;
+    f)
+      FRESH_BUILD="true"
+      ;;
     g)
       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
       ;;
@@ -121,7 +126,7 @@
 fi
 
 "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
+  "$ALL_SESSIONS" "$BUILD_HEAP" "$FRESH_BUILD" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
 RC="$?"
 
diff -r 38e225bd53e4 -r a125b8040ada src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Sat Jul 28 22:01:21 2012 +0200
+++ b/src/Pure/System/build.scala	Sun Jul 29 21:40:46 2012 +0200
@@ -440,6 +440,7 @@
     all_sessions: Boolean = false,
     build_heap: Boolean = false,
     more_dirs: List[Path] = Nil,
+    fresh_build: Boolean,
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     no_build: Boolean = false,
@@ -523,7 +524,7 @@
                     case None => false
                   }
                 }
-                val all_current = current && parent_current
+                val all_current = current && parent_current && !fresh_build
 
                 if (all_current)
                   loop(pending - name, running, results + (name -> (true, 0)))
@@ -571,13 +572,14 @@
         case
           Properties.Value.Boolean(all_sessions) ::
           Properties.Value.Boolean(build_heap) ::
+          Properties.Value.Boolean(fresh_build) ::
           Properties.Value.Int(max_jobs) ::
           Properties.Value.Boolean(no_build) ::
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
           Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
-            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
-              max_jobs, no_build, build_options, system_mode, verbose, sessions)
+            build(all_sessions, build_heap, more_dirs.map(Path.explode), fresh_build,
+              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }