tuned signature;
authorwenzelm
Fri Mar 17 21:55:13 2017 +0100 (2017-03-17)
changeset 65296a71db30f3b2d
parent 65295 5e4e7aaa4270
child 65297 dfbb17430342
tuned signature;
src/Pure/Admin/build_history.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Fri Mar 17 21:43:37 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_history.scala	Fri Mar 17 21:55:13 2017 +0100
     1.3 @@ -230,8 +230,7 @@
     1.4              val properties =
     1.5                if (database.is_file) {
     1.6                  using(SQLite.open_database(database))(db =>
     1.7 -                  Sessions.Session_Info.read_build_log(
     1.8 -                    store, db, session_name, ml_statistics = true)).ml_statistics
     1.9 +                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
    1.10                }
    1.11                else if (log_gz.is_file) {
    1.12                  Build_Log.Log_File(log_gz).
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Mar 17 21:43:37 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 21:55:13 2017 +0100
     2.3 @@ -515,6 +515,27 @@
     2.4  
     2.5    /** persistent store **/
     2.6  
     2.7 +  object Session_Info
     2.8 +  {
     2.9 +    // Build_Log.Session_Info
    2.10 +    val session_name = SQL.Column.string("session_name")
    2.11 +    val session_timing = SQL.Column.bytes("session_timing")
    2.12 +    val command_timings = SQL.Column.bytes("command_timings")
    2.13 +    val ml_statistics = SQL.Column.bytes("ml_statistics")
    2.14 +    val task_statistics = SQL.Column.bytes("task_statistics")
    2.15 +    val build_log_columns =
    2.16 +      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    2.17 +
    2.18 +    // Build.Session_Info
    2.19 +    val sources = SQL.Column.string("sources")
    2.20 +    val input_heaps = SQL.Column.string("input_heaps")
    2.21 +    val output_heap = SQL.Column.string("output_heap")
    2.22 +    val return_code = SQL.Column.int("return_code")
    2.23 +    val build_columns = List(sources, input_heaps, output_heap, return_code)
    2.24 +
    2.25 +    val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    2.26 +  }
    2.27 +
    2.28    def store(system_mode: Boolean = false): Store = new Store(system_mode)
    2.29  
    2.30    class Store private[Sessions](system_mode: Boolean)
    2.31 @@ -606,44 +627,23 @@
    2.32      /* print */
    2.33  
    2.34      override def toString: String = "Store(output_dir = " + output_dir.expand + ")"
    2.35 -  }
    2.36  
    2.37  
    2.38 -  /* session info */
    2.39 +    /* session info */
    2.40  
    2.41 -  object Session_Info
    2.42 -  {
    2.43 -    // Build_Log.Session_Info
    2.44 -    val session_name = SQL.Column.string("session_name")
    2.45 -    val session_timing = SQL.Column.bytes("session_timing")
    2.46 -    val command_timings = SQL.Column.bytes("command_timings")
    2.47 -    val ml_statistics = SQL.Column.bytes("ml_statistics")
    2.48 -    val task_statistics = SQL.Column.bytes("task_statistics")
    2.49 -    val build_log_columns =
    2.50 -      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    2.51 -
    2.52 -    // Build.Session_Info
    2.53 -    val sources = SQL.Column.string("sources")
    2.54 -    val input_heaps = SQL.Column.string("input_heaps")
    2.55 -    val output_heap = SQL.Column.string("output_heap")
    2.56 -    val return_code = SQL.Column.int("return_code")
    2.57 -    val build_columns = List(sources, input_heaps, output_heap, return_code)
    2.58 -
    2.59 -    val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    2.60 -
    2.61 -    def write(store: Store, db: SQL.Database,
    2.62 -      build_log: Build_Log.Session_Info, build: Build.Session_Info)
    2.63 +    def write_session_info(
    2.64 +      db: SQL.Database, build_log: Build_Log.Session_Info, build: Build.Session_Info)
    2.65      {
    2.66        db.transaction {
    2.67 -        db.drop_table(table)
    2.68 -        db.create_table(table)
    2.69 -        using(db.insert_statement(table))(stmt =>
    2.70 +        db.drop_table(Session_Info.table)
    2.71 +        db.create_table(Session_Info.table)
    2.72 +        using(db.insert_statement(Session_Info.table))(stmt =>
    2.73          {
    2.74            db.set_string(stmt, 1, build_log.session_name)
    2.75 -          db.set_bytes(stmt, 2, store.encode_properties(build_log.session_timing))
    2.76 -          db.set_bytes(stmt, 3, store.compress_properties(build_log.command_timings))
    2.77 -          db.set_bytes(stmt, 4, store.compress_properties(build_log.ml_statistics))
    2.78 -          db.set_bytes(stmt, 5, store.compress_properties(build_log.task_statistics))
    2.79 +          db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    2.80 +          db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
    2.81 +          db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
    2.82 +          db.set_bytes(stmt, 5, compress_properties(build_log.task_statistics))
    2.83            db.set_string(stmt, 6, cat_lines(build.sources))
    2.84            db.set_string(stmt, 7, cat_lines(build.input_heaps))
    2.85            db.set_string(stmt, 8, build.output_heap getOrElse "")
    2.86 @@ -653,48 +653,49 @@
    2.87        }
    2.88      }
    2.89  
    2.90 -    def read_session_timing(store: Store, db: SQL.Database): Properties.T =
    2.91 -      store.decode_properties(store.read_bytes(db, table, session_timing))
    2.92 +    def read_session_timing(db: SQL.Database): Properties.T =
    2.93 +      decode_properties(read_bytes(db, Session_Info.table, Session_Info.session_timing))
    2.94  
    2.95 -    def read_command_timings(store: Store, db: SQL.Database): List[Properties.T] =
    2.96 -      store.read_properties(db, table, command_timings)
    2.97 +    def read_command_timings(db: SQL.Database): List[Properties.T] =
    2.98 +      read_properties(db, Session_Info.table, Session_Info.command_timings)
    2.99  
   2.100 -    def read_ml_statistics(store: Store, db: SQL.Database): List[Properties.T] =
   2.101 -      store.read_properties(db, table, ml_statistics)
   2.102 +    def read_ml_statistics(db: SQL.Database): List[Properties.T] =
   2.103 +      read_properties(db, Session_Info.table, Session_Info.ml_statistics)
   2.104  
   2.105 -    def read_task_statistics(store: Store, db: SQL.Database): List[Properties.T] =
   2.106 -      store.read_properties(db, table, task_statistics)
   2.107 +    def read_task_statistics(db: SQL.Database): List[Properties.T] =
   2.108 +      read_properties(db, Session_Info.table, Session_Info.task_statistics)
   2.109  
   2.110 -    def read_build_log(store: Store, db: SQL.Database,
   2.111 +    def read_build_log(db: SQL.Database,
   2.112        default_name: String = "",
   2.113        command_timings: Boolean = false,
   2.114        ml_statistics: Boolean = false,
   2.115        task_statistics: Boolean = false): Build_Log.Session_Info =
   2.116      {
   2.117 -      val name = store.read_string(db, table, session_name)
   2.118 +      val name = read_string(db, Session_Info.table, Session_Info.session_name)
   2.119        Build_Log.Session_Info(
   2.120          session_name =
   2.121            if (name == "") default_name
   2.122            else if (default_name == "" || default_name == name) name
   2.123            else error("Database from different session " + quote(name)),
   2.124 -        session_timing = read_session_timing(store, db),
   2.125 -        command_timings = if (command_timings) read_command_timings(store, db) else Nil,
   2.126 -        ml_statistics = if (ml_statistics) read_ml_statistics(store, db) else Nil,
   2.127 -        task_statistics = if (task_statistics) read_task_statistics(store, db) else Nil)
   2.128 +        session_timing = read_session_timing(db),
   2.129 +        command_timings = if (command_timings) read_command_timings(db) else Nil,
   2.130 +        ml_statistics = if (ml_statistics) read_ml_statistics(db) else Nil,
   2.131 +        task_statistics = if (task_statistics) read_task_statistics(db) else Nil)
   2.132      }
   2.133  
   2.134 -    def read_build(store: Store, db: SQL.Database): Option[Build.Session_Info] =
   2.135 -      using(db.select_statement(table, table.columns))(stmt =>
   2.136 +    def read_build(db: SQL.Database): Option[Build.Session_Info] =
   2.137 +      using(db.select_statement(Session_Info.table, Session_Info.table.columns))(stmt =>
   2.138        {
   2.139          val rs = stmt.executeQuery
   2.140          if (!rs.next) None
   2.141          else {
   2.142            Some(
   2.143              Build.Session_Info(
   2.144 -              split_lines(db.string(rs, sources.name)),
   2.145 -              split_lines(db.string(rs, input_heaps.name)),
   2.146 -              db.string(rs, output_heap.name) match { case "" => None case s => Some(s) },
   2.147 -              db.int(rs, return_code.name)))
   2.148 +              split_lines(db.string(rs, Session_Info.sources.name)),
   2.149 +              split_lines(db.string(rs, Session_Info.input_heaps.name)),
   2.150 +              db.string(rs,
   2.151 +                Session_Info.output_heap.name) match { case "" => None case s => Some(s) },
   2.152 +              db.int(rs, Session_Info.return_code.name)))
   2.153          }
   2.154        })
   2.155    }
     3.1 --- a/src/Pure/Tools/build.scala	Fri Mar 17 21:43:37 2017 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Fri Mar 17 21:55:13 2017 +0100
     3.3 @@ -49,8 +49,7 @@
     3.4            try {
     3.5              using(SQLite.open_database(database))(db =>
     3.6              {
     3.7 -              val build_log =
     3.8 -                Sessions.Session_Info.read_build_log(store, db, name, command_timings = true)
     3.9 +              val build_log = store.read_build_log(db, name, command_timings = true)
    3.10                val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    3.11                (build_log.command_timings, session_timing)
    3.12              })
    3.13 @@ -424,7 +423,7 @@
    3.14                database.file.delete
    3.15  
    3.16                using(SQLite.open_database(database))(db =>
    3.17 -                Sessions.Session_Info.write(store, db,
    3.18 +                store.write_session_info(db,
    3.19                    build_log =
    3.20                      Build_Log.Log_File(name, process_result.out_lines).
    3.21                        parse_session_info(name,
    3.22 @@ -449,9 +448,7 @@
    3.23                  {
    3.24                    store.find_database_heap(name) match {
    3.25                      case Some((database, heap_stamp)) =>
    3.26 -                      using(SQLite.open_database(database))(
    3.27 -                        Sessions.Session_Info.read_build(store, _)) match
    3.28 -                      {
    3.29 +                      using(SQLite.open_database(database))(store.read_build(_)) match {
    3.30                          case Some(build) =>
    3.31                            val current =
    3.32                              build.sources == sources_stamp(name) &&