1.1 --- a/doc-src/System/Thy/Sessions.thy	Sat Jul 28 22:01:21 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Sessions.thy	Sun Jul 29 21:40:46 2012 +0200
     1.3 @@ -168,6 +168,7 @@
     1.4      -a           select all sessions
     1.5      -b           build heap images
     1.6      -d DIR       include session directory with ROOT file
     1.7 +    -f           fresh build
     1.8      -g NAME      select session group NAME
     1.9      -j INT       maximum number of parallel jobs (default 1)
    1.10      -n           no build -- test dependencies only
    1.11 @@ -221,6 +222,9 @@
    1.12    saved for inner nodes of the hierarchy of sessions, as required for
    1.13    other sessions to continue later on.
    1.14  
    1.15 +  \medskip Option @{verbatim "-f"} ensures a fresh build, even if all
    1.16 +  results are up-to-date wrt.\ the current set of sources.
    1.17 +
    1.18    \medskip Option @{verbatim "-j"} specifies the maximum number of
    1.19    parallel build jobs (prover processes).  Note that each process is
    1.20    subject to a separate limit of parallel threads, cf.\ system option

     2.1 --- a/doc-src/System/Thy/document/Sessions.tex	Sat Jul 28 22:01:21 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Sun Jul 29 21:40:46 2012 +0200
     2.3 @@ -278,6 +278,7 @@
     2.4      -a           select all sessions
     2.5      -b           build heap images
     2.6      -d DIR       include session directory with ROOT file
     2.7 +    -f           fresh build
     2.8      -g NAME      select session group NAME
     2.9      -j INT       maximum number of parallel jobs (default 1)
    2.10      -n           no build -- test dependencies only
    2.11 @@ -327,6 +328,9 @@
    2.12    saved for inner nodes of the hierarchy of sessions, as required for
    2.13    other sessions to continue later on.
    2.14  
    2.15 +  \medskip Option \verb|-f| ensures a fresh build, even if all
    2.16 +  results are up-to-date wrt.\ the current set of sources.
    2.17 +
    2.18    \medskip Option \verb|-j| specifies the maximum number of
    2.19    parallel build jobs (prover processes).  Note that each process is
    2.20    subject to a separate limit of parallel threads, cf.\ system option

     3.1 --- a/lib/Tools/build	Sat Jul 28 22:01:21 2012 +0200
     3.2 +++ b/lib/Tools/build	Sun Jul 29 21:40:46 2012 +0200
     3.3 @@ -29,6 +29,7 @@
     3.4    echo "    -a           select all sessions"
     3.5    echo "    -b           build heap images"
     3.6    echo "    -d DIR       include session directory with ROOT file"
     3.7 +  echo "    -f           fresh build"
     3.8    echo "    -g NAME      select session group NAME"
     3.9    echo "    -j INT       maximum number of parallel jobs (default 1)"
    3.10    echo "    -n           no build -- test dependencies only"
    3.11 @@ -59,6 +60,7 @@
    3.12  ALL_SESSIONS=false
    3.13  BUILD_HEAP=false
    3.14  declare -a MORE_DIRS=()
    3.15 +FRESH_BUILD=false
    3.16  declare -a SESSION_GROUPS=()
    3.17  MAX_JOBS=1
    3.18  NO_BUILD=false
    3.19 @@ -66,7 +68,7 @@
    3.20  SYSTEM_MODE=false
    3.21  VERBOSE=false
    3.22  
    3.23 -while getopts "abd:g:j:no:sv" OPT
    3.24 +while getopts "abd:fg:j:no:sv" OPT
    3.25  do
    3.26    case "$OPT" in
    3.27      a)
    3.28 @@ -78,6 +80,9 @@
    3.29      d)
    3.30        MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    3.31        ;;
    3.32 +    f)
    3.33 +      FRESH_BUILD="true"
    3.34 +      ;;
    3.35      g)
    3.36        SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
    3.37        ;;
    3.38 @@ -121,7 +126,7 @@
    3.39  fi
    3.40  
    3.41  "$ISABELLE_TOOL" java isabelle.Build \
    3.42 -  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    3.43 +  "$ALL_SESSIONS" "$BUILD_HEAP" "$FRESH_BUILD" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    3.44    "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    3.45  RC="$?"
    3.46  

     4.1 --- a/src/Pure/System/build.scala	Sat Jul 28 22:01:21 2012 +0200
     4.2 +++ b/src/Pure/System/build.scala	Sun Jul 29 21:40:46 2012 +0200
     4.3 @@ -440,6 +440,7 @@
     4.4      all_sessions: Boolean = false,
     4.5      build_heap: Boolean = false,
     4.6      more_dirs: List[Path] = Nil,
     4.7 +    fresh_build: Boolean,
     4.8      session_groups: List[String] = Nil,
     4.9      max_jobs: Int = 1,
    4.10      no_build: Boolean = false,
    4.11 @@ -523,7 +524,7 @@
    4.12                      case None => false
    4.13                    }
    4.14                  }
    4.15 -                val all_current = current && parent_current
    4.16 +                val all_current = current && parent_current && !fresh_build
    4.17  
    4.18                  if (all_current)
    4.19                    loop(pending - name, running, results + (name -> (true, 0)))
    4.20 @@ -571,13 +572,14 @@
    4.21          case
    4.22            Properties.Value.Boolean(all_sessions) ::
    4.23            Properties.Value.Boolean(build_heap) ::
    4.24 +          Properties.Value.Boolean(fresh_build) ::
    4.25            Properties.Value.Int(max_jobs) ::
    4.26            Properties.Value.Boolean(no_build) ::
    4.27            Properties.Value.Boolean(system_mode) ::
    4.28            Properties.Value.Boolean(verbose) ::
    4.29            Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
    4.30 -            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
    4.31 -              max_jobs, no_build, build_options, system_mode, verbose, sessions)
    4.32 +            build(all_sessions, build_heap, more_dirs.map(Path.explode), fresh_build,
    4.33 +              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
    4.34          case _ => error("Bad arguments:\n" + cat_lines(args))
    4.35        }
    4.36      }