748 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
748 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
749 } |
749 } |
750 |
750 |
751 def store(system_mode: Boolean = false): Store = new Store(system_mode) |
751 def store(system_mode: Boolean = false): Store = new Store(system_mode) |
752 |
752 |
753 class Store private[Sessions](system_mode: Boolean) extends Properties.Store |
753 class Store private[Sessions](system_mode: Boolean) |
754 { |
754 { |
755 /* file names */ |
755 /* file names */ |
756 |
756 |
757 def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") |
757 def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") |
758 def log(name: String): Path = Path.basic("log") + Path.basic(name) |
758 def log(name: String): Path = Path.basic("log") + Path.basic(name) |
759 def log_gz(name: String): Path = log(name).ext("gz") |
759 def log_gz(name: String): Path = log(name).ext("gz") |
760 |
760 |
761 |
761 |
762 /* SQL database content */ |
762 /* SQL database content */ |
|
763 |
|
764 val xml_cache = new XML.Cache() |
763 |
765 |
764 def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = |
766 def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = |
765 db.using_statement(Session_Info.table.select(List(column), |
767 db.using_statement(Session_Info.table.select(List(column), |
766 Session_Info.session_name.where_equal(name)))(stmt => |
768 Session_Info.session_name.where_equal(name)))(stmt => |
767 { |
769 { |
768 val res = stmt.execute_query() |
770 val res = stmt.execute_query() |
769 if (!res.next()) Bytes.empty else res.bytes(column) |
771 if (!res.next()) Bytes.empty else res.bytes(column) |
770 }) |
772 }) |
771 |
773 |
772 def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = |
774 def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = |
773 uncompress_properties(read_bytes(db, name, column)) |
775 Properties.uncompress(read_bytes(db, name, column), Some(xml_cache)) |
774 |
776 |
775 |
777 |
776 /* output */ |
778 /* output */ |
777 |
779 |
778 val browser_info: Path = |
780 val browser_info: Path = |
823 db.using_statement( |
825 db.using_statement( |
824 Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) |
826 Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) |
825 db.using_statement(Session_Info.table.insert())(stmt => |
827 db.using_statement(Session_Info.table.insert())(stmt => |
826 { |
828 { |
827 stmt.string(1) = name |
829 stmt.string(1) = name |
828 stmt.bytes(2) = encode_properties(build_log.session_timing) |
830 stmt.bytes(2) = Properties.encode(build_log.session_timing) |
829 stmt.bytes(3) = compress_properties(build_log.command_timings) |
831 stmt.bytes(3) = Properties.compress(build_log.command_timings) |
830 stmt.bytes(4) = compress_properties(build_log.ml_statistics) |
832 stmt.bytes(4) = Properties.compress(build_log.ml_statistics) |
831 stmt.bytes(5) = compress_properties(build_log.task_statistics) |
833 stmt.bytes(5) = Properties.compress(build_log.task_statistics) |
832 stmt.string(6) = cat_lines(build.sources) |
834 stmt.string(6) = cat_lines(build.sources) |
833 stmt.string(7) = cat_lines(build.input_heaps) |
835 stmt.string(7) = cat_lines(build.input_heaps) |
834 stmt.string(8) = build.output_heap getOrElse "" |
836 stmt.string(8) = build.output_heap getOrElse "" |
835 stmt.int(9) = build.return_code |
837 stmt.int(9) = build.return_code |
836 stmt.execute() |
838 stmt.execute() |
837 }) |
839 }) |
838 } |
840 } |
839 } |
841 } |
840 |
842 |
841 def read_session_timing(db: SQL.Database, name: String): Properties.T = |
843 def read_session_timing(db: SQL.Database, name: String): Properties.T = |
842 decode_properties(read_bytes(db, name, Session_Info.session_timing)) |
844 Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache)) |
843 |
845 |
844 def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = |
846 def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = |
845 read_properties(db, name, Session_Info.command_timings) |
847 read_properties(db, name, Session_Info.command_timings) |
846 |
848 |
847 def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] = |
849 def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] = |