src/Pure/Tools/build.scala
changeset 66746 888a51e77c6e
parent 66745 e7ac579b883c
child 66747 f4c6c8a8f645
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 02 11:43:17 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 13:33:36 2017 +0200
     1.3 @@ -24,7 +24,6 @@
     1.4    /* persistent build info */
     1.5  
     1.6    sealed case class Session_Info(
     1.7 -    imported_sources: List[String],
     1.8      sources: List[String],
     1.9      input_heaps: List[String],
    1.10      output_heap: Option[String],
    1.11 @@ -375,11 +374,9 @@
    1.12  
    1.13      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    1.14  
    1.15 -    def imported_sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    1.16 -      deps.imported_sources(name).map(_.toString).sorted
    1.17 -
    1.18      def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    1.19 -      (full_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    1.20 +      (full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name))
    1.21 +        .map(_.toString).sorted
    1.22  
    1.23      val (selected, selected_sessions, deps) =
    1.24      {
    1.25 @@ -401,7 +398,6 @@
    1.26                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.27                    case Some(build)
    1.28                    if build.return_code == 0 &&
    1.29 -                    build.imported_sources == imported_sources_stamp(deps0, name) &&
    1.30                      build.sources == sources_stamp(deps0, name) => None
    1.31                    case _ => Some(name)
    1.32                  }
    1.33 @@ -537,11 +533,7 @@
    1.34                        parse_session_info(
    1.35                          command_timings = true, ml_statistics = true, task_statistics = true),
    1.36                    build =
    1.37 -                    Session_Info(
    1.38 -                      imported_sources_stamp(deps, name),
    1.39 -                      sources_stamp(deps, name),
    1.40 -                      input_heaps,
    1.41 -                      heap_stamp,
    1.42 +                    Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    1.43                        process_result.rc)))
    1.44              }
    1.45