524 def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") |
524 def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") |
525 def log(name: String): Path = Path.basic("log") + Path.basic(name) |
525 def log(name: String): Path = Path.basic("log") + Path.basic(name) |
526 def log_gz(name: String): Path = log(name).ext("gz") |
526 def log_gz(name: String): Path = log(name).ext("gz") |
527 |
527 |
528 |
528 |
|
529 /* data representation */ |
|
530 |
|
531 val xml_cache: XML.Cache = new XML.Cache() |
|
532 |
|
533 def encode_properties(ps: Properties.T): Bytes = |
|
534 Bytes(YXML.string_of_body(XML.Encode.properties(ps))) |
|
535 |
|
536 def decode_properties(bs: Bytes): Properties.T = |
|
537 xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text))) |
|
538 |
|
539 def compress_properties(ps: List[Properties.T], options: XZ.Options = XZ.options()): Bytes = |
|
540 { |
|
541 if (ps.isEmpty) Bytes.empty |
|
542 else Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.properties)(ps))).compress(options) |
|
543 } |
|
544 |
|
545 def uncompress_properties(bs: Bytes): List[Properties.T] = |
|
546 { |
|
547 if (bs.isEmpty) Nil |
|
548 else |
|
549 XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress().text)). |
|
550 map(xml_cache.props(_)) |
|
551 } |
|
552 |
|
553 |
529 /* output */ |
554 /* output */ |
530 |
555 |
531 val browser_info: Path = |
556 val browser_info: Path = |
532 if (system_mode) Path.explode("~~/browser_info") |
557 if (system_mode) Path.explode("~~/browser_info") |
533 else Path.explode("$ISABELLE_BROWSER_INFO") |
558 else Path.explode("$ISABELLE_BROWSER_INFO") |
608 |
615 |
609 val table = SQL.Table("isabelle_session_info", |
616 val table = SQL.Table("isabelle_session_info", |
610 List(session_name, session_timing, command_timings, ml_statistics, task_statistics, |
617 List(session_name, session_timing, command_timings, ml_statistics, task_statistics, |
611 sources, input_heaps, output_heap, return_code)) |
618 sources, input_heaps, output_heap, return_code)) |
612 |
619 |
613 def write_data(db: SQLite.Database, info1: Build_Log.Session_Info, info2: Build.Session_Info) |
620 def write_data(store: Store, db: SQLite.Database, |
|
621 build_log: Build_Log.Session_Info, build: Build.Session_Info) |
614 { |
622 { |
615 db.transaction { |
623 db.transaction { |
616 db.drop_table(table) |
624 db.drop_table(table) |
617 db.create_table(table) |
625 db.create_table(table) |
618 using(db.insert_statement(table))(stmt => |
626 using(db.insert_statement(table))(stmt => |
619 { |
627 { |
620 db.set_string(stmt, 1, info1.session_name) |
628 db.set_string(stmt, 1, build_log.session_name) |
621 db.set_bytes(stmt, 2, encode_properties(info1.session_timing)) |
629 db.set_bytes(stmt, 2, store.encode_properties(build_log.session_timing)) |
622 db.set_bytes(stmt, 3, compress_properties(info1.command_timings)) |
630 db.set_bytes(stmt, 3, store.compress_properties(build_log.command_timings)) |
623 db.set_bytes(stmt, 4, compress_properties(info1.ml_statistics)) |
631 db.set_bytes(stmt, 4, store.compress_properties(build_log.ml_statistics)) |
624 db.set_bytes(stmt, 5, compress_properties(info1.task_statistics)) |
632 db.set_bytes(stmt, 5, store.compress_properties(build_log.task_statistics)) |
625 db.set_string(stmt, 6, info2.sources) |
633 db.set_string(stmt, 6, build.sources) |
626 db.set_string(stmt, 7, info2.input_heaps) |
634 db.set_string(stmt, 7, build.input_heaps) |
627 db.set_string(stmt, 8, info2.output_heap) |
635 db.set_string(stmt, 8, build.output_heap) |
628 db.set_int(stmt, 9, info2.return_code) |
636 db.set_int(stmt, 9, build.return_code) |
629 stmt.execute() |
637 stmt.execute() |
630 }) |
638 }) |
631 } |
639 } |
632 } |
640 } |
633 |
641 |
634 def read_data(db: SQLite.Database): Option[(Build_Log.Session_Info, Build.Session_Info)] = |
642 def read_data(store: Store, db: SQLite.Database) |
|
643 : Option[(Build_Log.Session_Info, Build.Session_Info)] = |
635 { |
644 { |
636 using(db.select_statement(table, table.columns))(stmt => |
645 using(db.select_statement(table, table.columns))(stmt => |
637 { |
646 { |
638 val rs = stmt.executeQuery |
647 val rs = stmt.executeQuery |
639 if (!rs.next) None |
648 if (!rs.next) None |
640 else { |
649 else { |
641 val info1 = |
650 val build_log = |
642 Build_Log.Session_Info( |
651 Build_Log.Session_Info( |
643 db.string(rs, session_name.name), |
652 db.string(rs, session_name.name), |
644 decode_properties(db.bytes(rs, session_timing.name)), |
653 store.decode_properties(db.bytes(rs, session_timing.name)), |
645 uncompress_properties(db.bytes(rs, command_timings.name)), |
654 store.uncompress_properties(db.bytes(rs, command_timings.name)), |
646 uncompress_properties(db.bytes(rs, ml_statistics.name)), |
655 store.uncompress_properties(db.bytes(rs, ml_statistics.name)), |
647 uncompress_properties(db.bytes(rs, task_statistics.name))) |
656 store.uncompress_properties(db.bytes(rs, task_statistics.name))) |
648 val info2 = |
657 val build = |
649 Build.Session_Info( |
658 Build.Session_Info( |
650 db.string(rs, sources.name), |
659 db.string(rs, sources.name), |
651 db.string(rs, input_heaps.name), |
660 db.string(rs, input_heaps.name), |
652 db.string(rs, output_heap.name), |
661 db.string(rs, output_heap.name), |
653 db.int(rs, return_code.name)) |
662 db.int(rs, return_code.name)) |
654 Some((info1, info2)) |
663 Some((build_log, build)) |
655 } |
664 } |
656 }) |
665 }) |
657 } |
666 } |
658 } |
667 } |
659 } |
668 } |