src/Pure/Tools/build.scala
changeset 65320 52861eebf58d
parent 65318 342efc382558
child 65344 b99283eed13c
equal deleted inserted replaced
65319:64da14387b2c 65320:52861eebf58d
    47             no_timings
    47             no_timings
    48           }
    48           }
    49           try {
    49           try {
    50             using(SQLite.open_database(database))(db =>
    50             using(SQLite.open_database(database))(db =>
    51             {
    51             {
    52               val build_log = store.read_build_log(db, command_timings = true)
    52               val build_log = store.read_build_log(db, name, command_timings = true)
    53               val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    53               val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    54               (build_log.command_timings, session_timing)
    54               (build_log.command_timings, session_timing)
    55             })
    55             })
    56           }
    56           }
    57           catch {
    57           catch {
   523 
   523 
   524                 val (current, heap_stamp) =
   524                 val (current, heap_stamp) =
   525                 {
   525                 {
   526                   store.find_database_heap(name) match {
   526                   store.find_database_heap(name) match {
   527                     case Some((database, heap_stamp)) =>
   527                     case Some((database, heap_stamp)) =>
   528                       using(SQLite.open_database(database))(store.read_build(_)) match {
   528                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   529                         case Some(build) =>
   529                         case Some(build) =>
   530                           val current =
   530                           val current =
   531                             build.sources == sources_stamp(name) &&
   531                             build.sources == sources_stamp(name) &&
   532                             build.input_heaps == ancestor_heaps &&
   532                             build.input_heaps == ancestor_heaps &&
   533                             build.output_heap == heap_stamp &&
   533                             build.output_heap == heap_stamp &&