more selective database access;
authorwenzelm
Fri May 26 15:28:46 2017 +0200 (24 months ago)
changeset 6593573c099fa96a4
parent 65934 5f202ba9f590
child 65936 aece72468de5
more selective database access;
src/Pure/Admin/build_history.scala
src/Pure/Admin/jenkins.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Fri May 26 15:19:21 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_history.scala	Fri May 26 15:28:46 2017 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4              val properties =
     1.5                if (database.is_file) {
     1.6                  using(SQLite.open_database(database))(db =>
     1.7 -                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
     1.8 +                  store.read_ml_statistics(db, session_name))
     1.9                }
    1.10                else if (log_gz.is_file) {
    1.11                  Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
     2.1 --- a/src/Pure/Admin/jenkins.scala	Fri May 26 15:19:21 2017 +0200
     2.2 +++ b/src/Pure/Admin/jenkins.scala	Fri May 26 15:28:46 2017 +0200
     2.3 @@ -84,8 +84,7 @@
     2.4          case Some(url) =>
     2.5            Isabelle_System.with_tmp_file(session_name, "db") { database =>
     2.6              Bytes.write(database, Bytes.read(url))
     2.7 -            using(SQLite.open_database(database))(db =>
     2.8 -              store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
     2.9 +            using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name))
    2.10            }
    2.11          case None =>
    2.12            get_log("gz") match {
     3.1 --- a/src/Pure/Tools/build.scala	Fri May 26 15:19:21 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Fri May 26 15:28:46 2017 +0200
     3.3 @@ -51,9 +51,13 @@
     3.4            try {
     3.5              using(SQLite.open_database(database))(db =>
     3.6              {
     3.7 -              val build_log = store.read_build_log(db, name, command_timings = true)
     3.8 -              val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
     3.9 -              (build_log.command_timings, session_timing)
    3.10 +              val command_timings = store.read_command_timings(db, name)
    3.11 +              val session_timing =
    3.12 +                store.read_session_timing(db, name) match {
    3.13 +                  case Markup.Elapsed(t) => t
    3.14 +                  case _ => 0.0
    3.15 +                }
    3.16 +              (command_timings, session_timing)
    3.17              })
    3.18            }
    3.19            catch {