# HG changeset patch
# User wenzelm
# Date 1507745760 -7200
# Node ID 5c32a072ca8bf303be63ccaa999c5843548e75e1
# Parent  0d689d71dbdc0fc371d6820d65a26ec55b5fbfb2
added isablle build option -f;

diff -r 0d689d71dbdc -r 5c32a072ca8b NEWS
--- a/NEWS	Mon Oct 09 19:10:52 2017 +0200
+++ b/NEWS	Wed Oct 11 20:16:00 2017 +0200
@@ -69,6 +69,7 @@
 * Command-line tool "isabelle build" supports new options:
   - option -B NAME: include session NAME and all descendants
   - option -S: only observe changes of sources, not heap images
+  - option -f: forces a fresh build
 
 
 New in Isabelle2017 (October 2017)
diff -r 0d689d71dbdc -r 5c32a072ca8b src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Oct 09 19:10:52 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Oct 11 20:16:00 2017 +0200
@@ -280,6 +280,7 @@
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
@@ -365,6 +366,10 @@
   performing the specified build operation.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
+  requirements.
+
+  \<^medskip>
   Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
   (including optional cleanup). Note that the return code always indicates the
   status of the set of selected sessions.
diff -r 0d689d71dbdc -r 5c32a072ca8b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 09 19:10:52 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Oct 11 20:16:00 2017 +0200
@@ -354,6 +354,7 @@
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
+    fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
     system_mode: Boolean = false,
@@ -396,7 +397,7 @@
           verbose = verbose, list_files = list_files, check_keywords = check_keywords,
           global_theories = full_sessions.global_theories).check_errors
 
-      if (soft_build) {
+      if (soft_build && !fresh_build) {
         val outdated =
           selected0.flatMap(name =>
             store.find_database(name) match {
@@ -571,6 +572,7 @@
                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
                         case Some(build) =>
                           val current =
+                            !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, name) &&
                             build.input_heaps == ancestor_heaps &&
@@ -677,6 +679,7 @@
     var build_heap = false
     var clean_build = false
     var dirs: List[Path] = Nil
+    var fresh_build = false
     var session_groups: List[String] = Nil
     var max_jobs = 1
     var check_keywords: Set[String] = Set.empty
@@ -702,6 +705,7 @@
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
@@ -726,6 +730,7 @@
       "b" -> (_ => build_heap = true),
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "f" -> (_ => fresh_build = true),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
@@ -761,6 +766,7 @@
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,
+          fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           system_mode = system_mode,