src/Pure/Thy/sessions.scala
changeset 65295 5e4e7aaa4270
parent 65291 57c85c83c11b
child 65296 a71db30f3b2d
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Mar 17 21:18:49 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 21:43:37 2017 +0100
     1.3 @@ -550,21 +550,21 @@
     1.4            map(xml_cache.props(_))
     1.5      }
     1.6  
     1.7 -    def read_string(db: SQLite.Database, table: SQL.Table, column: SQL.Column): String =
     1.8 +    def read_string(db: SQL.Database, table: SQL.Table, column: SQL.Column): String =
     1.9        using(db.select_statement(table, List(column)))(stmt =>
    1.10        {
    1.11          val rs = stmt.executeQuery
    1.12          if (!rs.next) "" else db.string(rs, column.name)
    1.13        })
    1.14  
    1.15 -    def read_bytes(db: SQLite.Database, table: SQL.Table, column: SQL.Column): Bytes =
    1.16 +    def read_bytes(db: SQL.Database, table: SQL.Table, column: SQL.Column): Bytes =
    1.17        using(db.select_statement(table, List(column)))(stmt =>
    1.18        {
    1.19          val rs = stmt.executeQuery
    1.20          if (!rs.next) Bytes.empty else db.bytes(rs, column.name)
    1.21        })
    1.22  
    1.23 -    def read_properties(db: SQLite.Database, table: SQL.Table, column: SQL.Column)
    1.24 +    def read_properties(db: SQL.Database, table: SQL.Table, column: SQL.Column)
    1.25        : List[Properties.T] = uncompress_properties(read_bytes(db, table, column))
    1.26  
    1.27  
    1.28 @@ -631,7 +631,7 @@
    1.29  
    1.30      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    1.31  
    1.32 -    def write(store: Store, db: SQLite.Database,
    1.33 +    def write(store: Store, db: SQL.Database,
    1.34        build_log: Build_Log.Session_Info, build: Build.Session_Info)
    1.35      {
    1.36        db.transaction {
    1.37 @@ -653,19 +653,19 @@
    1.38        }
    1.39      }
    1.40  
    1.41 -    def read_session_timing(store: Store, db: SQLite.Database): Properties.T =
    1.42 +    def read_session_timing(store: Store, db: SQL.Database): Properties.T =
    1.43        store.decode_properties(store.read_bytes(db, table, session_timing))
    1.44  
    1.45 -    def read_command_timings(store: Store, db: SQLite.Database): List[Properties.T] =
    1.46 +    def read_command_timings(store: Store, db: SQL.Database): List[Properties.T] =
    1.47        store.read_properties(db, table, command_timings)
    1.48  
    1.49 -    def read_ml_statistics(store: Store, db: SQLite.Database): List[Properties.T] =
    1.50 +    def read_ml_statistics(store: Store, db: SQL.Database): List[Properties.T] =
    1.51        store.read_properties(db, table, ml_statistics)
    1.52  
    1.53 -    def read_task_statistics(store: Store, db: SQLite.Database): List[Properties.T] =
    1.54 +    def read_task_statistics(store: Store, db: SQL.Database): List[Properties.T] =
    1.55        store.read_properties(db, table, task_statistics)
    1.56  
    1.57 -    def read_build_log(store: Store, db: SQLite.Database,
    1.58 +    def read_build_log(store: Store, db: SQL.Database,
    1.59        default_name: String = "",
    1.60        command_timings: Boolean = false,
    1.61        ml_statistics: Boolean = false,
    1.62 @@ -683,7 +683,7 @@
    1.63          task_statistics = if (task_statistics) read_task_statistics(store, db) else Nil)
    1.64      }
    1.65  
    1.66 -    def read_build(store: Store, db: SQLite.Database): Option[Build.Session_Info] =
    1.67 +    def read_build(store: Store, db: SQL.Database): Option[Build.Session_Info] =
    1.68        using(db.select_statement(table, table.columns))(stmt =>
    1.69        {
    1.70          val rs = stmt.executeQuery