src/Pure/Tools/build.scala
changeset 65296 a71db30f3b2d
parent 65294 69100bf4ead4
child 65307 c1ba192b4f96
     1.1 --- a/src/Pure/Tools/build.scala	Fri Mar 17 21:43:37 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 21:55:13 2017 +0100
     1.3 @@ -49,8 +49,7 @@
     1.4            try {
     1.5              using(SQLite.open_database(database))(db =>
     1.6              {
     1.7 -              val build_log =
     1.8 -                Sessions.Session_Info.read_build_log(store, db, name, command_timings = true)
     1.9 +              val build_log = store.read_build_log(db, name, command_timings = true)
    1.10                val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    1.11                (build_log.command_timings, session_timing)
    1.12              })
    1.13 @@ -424,7 +423,7 @@
    1.14                database.file.delete
    1.15  
    1.16                using(SQLite.open_database(database))(db =>
    1.17 -                Sessions.Session_Info.write(store, db,
    1.18 +                store.write_session_info(db,
    1.19                    build_log =
    1.20                      Build_Log.Log_File(name, process_result.out_lines).
    1.21                        parse_session_info(name,
    1.22 @@ -449,9 +448,7 @@
    1.23                  {
    1.24                    store.find_database_heap(name) match {
    1.25                      case Some((database, heap_stamp)) =>
    1.26 -                      using(SQLite.open_database(database))(
    1.27 -                        Sessions.Session_Info.read_build(store, _)) match
    1.28 -                      {
    1.29 +                      using(SQLite.open_database(database))(store.read_build(_)) match {
    1.30                          case Some(build) =>
    1.31                            val current =
    1.32                              build.sources == sources_stamp(name) &&