# HG changeset patch
# User wenzelm
# Date 1343639024 -7200
# Node ID c24907e5081e3ab280c77af531c926c013c255c5
# Parent  c895e334162ce06b9a6cbad35ad4c8cdfebb57df
removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;

diff -r c895e334162c -r c24907e5081e doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Sun Jul 29 21:55:56 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Mon Jul 30 11:03:44 2012 +0200
@@ -168,7 +168,6 @@
     -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
@@ -222,9 +221,6 @@
   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 c895e334162c -r c24907e5081e doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Sun Jul 29 21:55:56 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Mon Jul 30 11:03:44 2012 +0200
@@ -278,7 +278,6 @@
     -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
@@ -328,9 +327,6 @@
   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 c895e334162c -r c24907e5081e lib/Tools/build
--- a/lib/Tools/build	Sun Jul 29 21:55:56 2012 +0200
+++ b/lib/Tools/build	Mon Jul 30 11:03:44 2012 +0200
@@ -29,7 +29,6 @@
   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"
@@ -60,7 +59,6 @@
 ALL_SESSIONS=false
 BUILD_HEAP=false
 declare -a MORE_DIRS=()
-FRESH_BUILD=false
 declare -a SESSION_GROUPS=()
 MAX_JOBS=1
 NO_BUILD=false
@@ -68,7 +66,7 @@
 SYSTEM_MODE=false
 VERBOSE=false
 
-while getopts "abd:fg:j:no:sv" OPT
+while getopts "abd:g:j:no:sv" OPT
 do
   case "$OPT" in
     a)
@@ -80,9 +78,6 @@
     d)
       MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
       ;;
-    f)
-      FRESH_BUILD="true"
-      ;;
     g)
       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
       ;;
@@ -126,7 +121,7 @@
 fi
 
 "$ISABELLE_TOOL" java isabelle.Build \
-  "$ALL_SESSIONS" "$BUILD_HEAP" "$FRESH_BUILD" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
+  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
 RC="$?"
 
diff -r c895e334162c -r c24907e5081e src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Sun Jul 29 21:55:56 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Jul 30 11:03:44 2012 +0200
@@ -440,7 +440,6 @@
     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,
@@ -524,7 +523,7 @@
                     case None => false
                   }
                 }
-                val all_current = current && parent_current && !fresh_build
+                val all_current = current && parent_current
 
                 if (all_current)
                   loop(pending - name, running, results + (name -> (true, 0)))
@@ -572,14 +571,13 @@
         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), fresh_build,
-              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
+            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
+              max_jobs, no_build, build_options, system_mode, verbose, sessions)
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }