src/Pure/Tools/build.scala
changeset 66841 5c32a072ca8b
parent 66822 4642cf4a7ebb
child 66848 982baed14542
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 09 19:10:52 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Oct 11 20:16:00 2017 +0200
     1.3 @@ -354,6 +354,7 @@
     1.4      max_jobs: Int = 1,
     1.5      list_files: Boolean = false,
     1.6      check_keywords: Set[String] = Set.empty,
     1.7 +    fresh_build: Boolean = false,
     1.8      no_build: Boolean = false,
     1.9      soft_build: Boolean = false,
    1.10      system_mode: Boolean = false,
    1.11 @@ -396,7 +397,7 @@
    1.12            verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    1.13            global_theories = full_sessions.global_theories).check_errors
    1.14  
    1.15 -      if (soft_build) {
    1.16 +      if (soft_build && !fresh_build) {
    1.17          val outdated =
    1.18            selected0.flatMap(name =>
    1.19              store.find_database(name) match {
    1.20 @@ -571,6 +572,7 @@
    1.21                        using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.22                          case Some(build) =>
    1.23                            val current =
    1.24 +                            !fresh_build &&
    1.25                              build.ok &&
    1.26                              build.sources == sources_stamp(deps, name) &&
    1.27                              build.input_heaps == ancestor_heaps &&
    1.28 @@ -677,6 +679,7 @@
    1.29      var build_heap = false
    1.30      var clean_build = false
    1.31      var dirs: List[Path] = Nil
    1.32 +    var fresh_build = false
    1.33      var session_groups: List[String] = Nil
    1.34      var max_jobs = 1
    1.35      var check_keywords: Set[String] = Set.empty
    1.36 @@ -702,6 +705,7 @@
    1.37      -b           build heap images
    1.38      -c           clean build
    1.39      -d DIR       include session directory
    1.40 +    -f           fresh build
    1.41      -g NAME      select session group NAME
    1.42      -j INT       maximum number of parallel jobs (default 1)
    1.43      -k KEYWORD   check theory sources for conflicts with proposed keywords
    1.44 @@ -726,6 +730,7 @@
    1.45        "b" -> (_ => build_heap = true),
    1.46        "c" -> (_ => clean_build = true),
    1.47        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    1.48 +      "f" -> (_ => fresh_build = true),
    1.49        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    1.50        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    1.51        "k:" -> (arg => check_keywords = check_keywords + arg),
    1.52 @@ -761,6 +766,7 @@
    1.53            max_jobs = max_jobs,
    1.54            list_files = list_files,
    1.55            check_keywords = check_keywords,
    1.56 +          fresh_build = fresh_build,
    1.57            no_build = no_build,
    1.58            soft_build = soft_build,
    1.59            system_mode = system_mode,