971 def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") |
971 def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") |
972 def log(name: String): Path = Path.basic("log") + Path.basic(name) |
972 def log(name: String): Path = Path.basic("log") + Path.basic(name) |
973 def log_gz(name: String): Path = log(name).ext("gz") |
973 def log_gz(name: String): Path = log(name).ext("gz") |
974 |
974 |
975 |
975 |
|
976 /* output */ |
|
977 |
|
978 val browser_info: Path = |
|
979 if (system_mode) Path.explode("~~/browser_info") |
|
980 else Path.explode("$ISABELLE_BROWSER_INFO") |
|
981 |
|
982 val output_dir: Path = |
|
983 if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER") |
|
984 else Path.explode("$ISABELLE_OUTPUT") |
|
985 |
|
986 override def toString: String = "Store(output_dir = " + output_dir.expand + ")" |
|
987 |
|
988 def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) } |
|
989 |
|
990 def output_heap(name: String): Path = output_dir + Path.basic(name) |
|
991 def output_log(name: String): Path = output_dir + log(name) |
|
992 def output_log_gz(name: String): Path = output_dir + log_gz(name) |
|
993 |
|
994 def open_output_database(name: String): SQL.Database = |
|
995 SQLite.open_database(output_dir + database(name)) |
|
996 |
|
997 |
|
998 /* input */ |
|
999 |
|
1000 private val input_dirs = |
|
1001 if (system_mode) List(output_dir) |
|
1002 else { |
|
1003 val ml_ident = Path.explode("$ML_IDENTIFIER").expand |
|
1004 output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident) |
|
1005 } |
|
1006 |
|
1007 def find_heap(name: String): Option[Path] = |
|
1008 input_dirs.map(_ + Path.basic(name)).find(_.is_file) |
|
1009 |
|
1010 def find_heap_digest(name: String): Option[String] = |
|
1011 find_heap(name).flatMap(read_heap_digest(_)) |
|
1012 |
|
1013 def find_database(name: String): Option[Path] = |
|
1014 input_dirs.map(_ + database(name)).find(_.is_file) |
|
1015 |
|
1016 def try_open_database(name: String): Option[SQL.Database] = |
|
1017 find_database(name).map(SQLite.open_database(_)) |
|
1018 |
|
1019 private def error_input(msg: String): Nothing = |
|
1020 error(msg + " -- expected in:\n" + cat_lines(input_dirs.map(dir => " " + dir.expand.implode))) |
|
1021 |
|
1022 def heap(name: String): Path = |
|
1023 find_heap(name) getOrElse error_input("Missing heap image for session " + quote(name)) |
|
1024 |
|
1025 def open_database(name: String): SQL.Database = |
|
1026 try_open_database(name) getOrElse error("Missing database file for session " + quote(name)) |
|
1027 |
|
1028 |
976 /* SQL database content */ |
1029 /* SQL database content */ |
977 |
1030 |
978 val xml_cache = XML.make_cache() |
1031 val xml_cache = XML.make_cache() |
979 val xz_cache = XZ.make_cache() |
1032 val xz_cache = XZ.make_cache() |
980 |
1033 |
987 }) |
1040 }) |
988 |
1041 |
989 def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = |
1042 def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = |
990 Properties.uncompress( |
1043 Properties.uncompress( |
991 read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache)) |
1044 read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache)) |
992 |
|
993 |
|
994 /* output */ |
|
995 |
|
996 val browser_info: Path = |
|
997 if (system_mode) Path.explode("~~/browser_info") |
|
998 else Path.explode("$ISABELLE_BROWSER_INFO") |
|
999 |
|
1000 val output_dir: Path = |
|
1001 if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER") |
|
1002 else Path.explode("$ISABELLE_OUTPUT") |
|
1003 |
|
1004 override def toString: String = "Store(output_dir = " + output_dir.expand + ")" |
|
1005 |
|
1006 def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) } |
|
1007 |
|
1008 def output_heap(name: String): Path = output_dir + Path.basic(name) |
|
1009 def output_log(name: String): Path = output_dir + log(name) |
|
1010 def output_log_gz(name: String): Path = output_dir + log_gz(name) |
|
1011 |
|
1012 def open_output_database(name: String): SQL.Database = |
|
1013 SQLite.open_database(output_dir + database(name)) |
|
1014 |
|
1015 |
|
1016 /* input */ |
|
1017 |
|
1018 private val input_dirs = |
|
1019 if (system_mode) List(output_dir) |
|
1020 else { |
|
1021 val ml_ident = Path.explode("$ML_IDENTIFIER").expand |
|
1022 output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident) |
|
1023 } |
|
1024 |
|
1025 def find_heap(name: String): Option[Path] = |
|
1026 input_dirs.map(_ + Path.basic(name)).find(_.is_file) |
|
1027 |
|
1028 def find_heap_digest(name: String): Option[String] = |
|
1029 find_heap(name).flatMap(read_heap_digest(_)) |
|
1030 |
|
1031 def find_database(name: String): Option[Path] = |
|
1032 input_dirs.map(_ + database(name)).find(_.is_file) |
|
1033 |
|
1034 def try_open_database(name: String): Option[SQL.Database] = |
|
1035 find_database(name).map(SQLite.open_database(_)) |
|
1036 |
|
1037 private def error_input(msg: String): Nothing = |
|
1038 error(msg + " -- expected in:\n" + cat_lines(input_dirs.map(dir => " " + dir.expand.implode))) |
|
1039 |
|
1040 def heap(name: String): Path = |
|
1041 find_heap(name) getOrElse error_input("Missing heap image for session " + quote(name)) |
|
1042 |
|
1043 def open_database(name: String): SQL.Database = |
|
1044 try_open_database(name) getOrElse error("Missing database file for session " + quote(name)) |
|
1045 |
1045 |
1046 |
1046 |
1047 /* session info */ |
1047 /* session info */ |
1048 |
1048 |
1049 def init_session_info(db: SQL.Database, name: String) |
1049 def init_session_info(db: SQL.Database, name: String) |