equal
deleted
inserted
replaced
745 val output_heap = SQL.Column.string("output_heap") |
745 val output_heap = SQL.Column.string("output_heap") |
746 val return_code = SQL.Column.int("return_code") |
746 val return_code = SQL.Column.int("return_code") |
747 val build_columns = List(sources, input_heaps, output_heap, return_code) |
747 val build_columns = List(sources, input_heaps, output_heap, return_code) |
748 |
748 |
749 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
749 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
750 |
|
751 def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column]) |
|
752 : PreparedStatement = |
|
753 db.select_statement(table, columns, session_name.sql_where_equal(name)) |
|
754 |
|
755 def delete_statement(db: SQL.Database, name: String): PreparedStatement = |
|
756 db.delete_statement(table, session_name.sql_where_equal(name)) |
|
757 } |
750 } |
758 |
751 |
759 def store(system_mode: Boolean = false): Store = new Store(system_mode) |
752 def store(system_mode: Boolean = false): Store = new Store(system_mode) |
760 |
753 |
761 class Store private[Sessions](system_mode: Boolean) extends Properties.Store |
754 class Store private[Sessions](system_mode: Boolean) extends Properties.Store |
768 |
761 |
769 |
762 |
770 /* SQL database content */ |
763 /* SQL database content */ |
771 |
764 |
772 def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = |
765 def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = |
773 using(Session_Info.select_statement(db, name, List(column)))(stmt => |
766 using(db.select_statement(Session_Info.table, List(column), |
|
767 Session_Info.session_name.sql_where_equal(name)))(stmt => |
774 { |
768 { |
775 val rs = stmt.executeQuery |
769 val rs = stmt.executeQuery |
776 if (!rs.next) Bytes.empty else db.bytes(rs, column) |
770 if (!rs.next) Bytes.empty else db.bytes(rs, column) |
777 }) |
771 }) |
778 |
772 |
825 build_log: Build_Log.Session_Info, |
819 build_log: Build_Log.Session_Info, |
826 build: Build.Session_Info) |
820 build: Build.Session_Info) |
827 { |
821 { |
828 db.transaction { |
822 db.transaction { |
829 db.create_table(Session_Info.table) |
823 db.create_table(Session_Info.table) |
830 using(Session_Info.delete_statement(db, name))(_.execute) |
824 using(db.delete_statement(Session_Info.table, |
|
825 Session_Info.session_name.sql_where_equal(name)))(_.execute) |
831 using(db.insert_statement(Session_Info.table))(stmt => |
826 using(db.insert_statement(Session_Info.table))(stmt => |
832 { |
827 { |
833 db.set_string(stmt, 1, name) |
828 db.set_string(stmt, 1, name) |
834 db.set_bytes(stmt, 2, encode_properties(build_log.session_timing)) |
829 db.set_bytes(stmt, 2, encode_properties(build_log.session_timing)) |
835 db.set_bytes(stmt, 3, compress_properties(build_log.command_timings)) |
830 db.set_bytes(stmt, 3, compress_properties(build_log.command_timings)) |
867 ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil, |
862 ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil, |
868 task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil) |
863 task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil) |
869 } |
864 } |
870 |
865 |
871 def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = |
866 def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = |
872 using(Session_Info.select_statement(db, name, Session_Info.build_columns))(stmt => |
867 using(db.select_statement(Session_Info.table, Session_Info.build_columns, |
|
868 Session_Info.session_name.sql_where_equal(name)))(stmt => |
873 { |
869 { |
874 val rs = stmt.executeQuery |
870 val rs = stmt.executeQuery |
875 if (!rs.next) None |
871 if (!rs.next) None |
876 else { |
872 else { |
877 Some( |
873 Some( |