819 } |
819 } |
820 |
820 |
821 deps |
821 deps |
822 } |
822 } |
823 |
823 |
|
824 def hierarchy(session: String): List[String] = build_graph.all_preds(List(session)) |
|
825 |
824 def build_selection(sel: Selection): List[String] = selected(build_graph, sel) |
826 def build_selection(sel: Selection): List[String] = selected(build_graph, sel) |
825 def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) |
827 def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) |
826 def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) |
828 def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) |
827 def build_topological_order: List[String] = build_graph.topological_order |
829 def build_topological_order: List[String] = build_graph.topological_order |
828 |
830 |
1192 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
1194 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
1193 } |
1195 } |
1194 |
1196 |
1195 class Database_Context private[Sessions]( |
1197 class Database_Context private[Sessions]( |
1196 val store: Sessions.Store, |
1198 val store: Sessions.Store, |
1197 val sessions_structure: Sessions.Structure, |
|
1198 database_server: Option[SQL.Database]) extends AutoCloseable |
1199 database_server: Option[SQL.Database]) extends AutoCloseable |
1199 { |
1200 { |
1200 def xml_cache: XML.Cache = store.xml_cache |
1201 def xml_cache: XML.Cache = store.xml_cache |
1201 def xz_cache: XZ.Cache = store.xz_cache |
1202 def xz_cache: XZ.Cache = store.xz_cache |
1202 |
1203 |
1216 case Some(db) => using(db)(f(_, session)) |
1217 case Some(db) => using(db)(f(_, session)) |
1217 case None => None |
1218 case None => None |
1218 } |
1219 } |
1219 } |
1220 } |
1220 |
1221 |
1221 def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] = |
1222 def read_export( |
1222 { |
1223 sessions: List[String], theory_name: String, name: String): Option[Export.Entry] = |
1223 val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view |
1224 { |
1224 val attempts = |
1225 val attempts = |
1225 database_server match { |
1226 database_server match { |
1226 case Some(db) => |
1227 case Some(db) => |
1227 hierarchy.map(session_name => |
1228 sessions.view.map(session_name => |
1228 Export.read_entry(db, store.xz_cache, session_name, theory_name, name)) |
1229 Export.read_entry(db, store.xz_cache, session_name, theory_name, name)) |
1229 case None => |
1230 case None => |
1230 hierarchy.map(session_name => |
1231 sessions.view.map(session_name => |
1231 store.try_open_database(session_name) match { |
1232 store.try_open_database(session_name) match { |
1232 case Some(db) => |
1233 case Some(db) => |
1233 using(db)(Export.read_entry(_, store.xz_cache, session_name, theory_name, name)) |
1234 using(db)(Export.read_entry(_, store.xz_cache, session_name, theory_name, name)) |
1234 case None => None |
1235 case None => None |
1235 }) |
1236 }) |
1236 } |
1237 } |
1237 attempts.collectFirst({ case Some(entry) => entry }) |
1238 attempts.collectFirst({ case Some(entry) => entry }) |
1238 } |
1239 } |
1239 |
1240 |
1240 def get_export(session: String, theory_name: String, name: String): Export.Entry = |
1241 def get_export( |
1241 read_export(session, theory_name, name) getOrElse |
1242 session_hierarchy: List[String], theory_name: String, name: String): Export.Entry = |
1242 Export.empty_entry(session, theory_name, name) |
1243 read_export(session_hierarchy, theory_name, name) getOrElse |
|
1244 Export.empty_entry(theory_name, name) |
1243 |
1245 |
1244 override def toString: String = |
1246 override def toString: String = |
1245 { |
1247 { |
1246 val s = |
1248 val s = |
1247 database_server match { |
1249 database_server match { |
1329 host = ssh_host, |
1331 host = ssh_host, |
1330 user = options.string("build_database_ssh_user"), |
1332 user = options.string("build_database_ssh_user"), |
1331 port = options.int("build_database_ssh_port"))), |
1333 port = options.int("build_database_ssh_port"))), |
1332 ssh_close = true) |
1334 ssh_close = true) |
1333 |
1335 |
1334 def open_database_context(sessions_structure: Sessions.Structure): Database_Context = |
1336 def open_database_context(): Database_Context = |
1335 new Database_Context(store, sessions_structure, |
1337 new Database_Context(store, if (database_server) Some(open_database_server()) else None) |
1336 if (database_server) Some(open_database_server()) else None) |
|
1337 |
1338 |
1338 def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = |
1339 def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = |
1339 { |
1340 { |
1340 def check(db: SQL.Database): Option[SQL.Database] = |
1341 def check(db: SQL.Database): Option[SQL.Database] = |
1341 if (output || session_info_exists(db)) Some(db) else { db.close; None } |
1342 if (output || session_info_exists(db)) Some(db) else { db.close; None } |