1178 val build_columns = List(sources, input_heaps, output_heap, return_code) |
1178 val build_columns = List(sources, input_heaps, output_heap, return_code) |
1179 |
1179 |
1180 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
1180 val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
1181 } |
1181 } |
1182 |
1182 |
|
1183 class Database_Context private[Sessions]( |
|
1184 val store: Sessions.Store, |
|
1185 sessions_structure: Sessions.Structure, |
|
1186 database_server: Option[SQL.Database]) extends AutoCloseable |
|
1187 { |
|
1188 def close { database_server.foreach(_.close) } |
|
1189 |
|
1190 def try_export(session: String, theory_name: String, name: String): Option[Export.Entry] = |
|
1191 { |
|
1192 val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view |
|
1193 val attempts = |
|
1194 database_server match { |
|
1195 case Some(db) => |
|
1196 hierarchy.map(session_name => Export.read_entry(db, session_name, theory_name, name)) |
|
1197 case None => |
|
1198 hierarchy.map(session_name => |
|
1199 store.try_open_database(session_name) match { |
|
1200 case Some(db) => using(db)(Export.read_entry(_, session_name, theory_name, name)) |
|
1201 case None => None |
|
1202 }) |
|
1203 } |
|
1204 attempts.collectFirst({ case Some(entry) => entry }) |
|
1205 } |
|
1206 |
|
1207 def export(session: String, theory_name: String, name: String): Export.Entry = |
|
1208 try_export(session, theory_name, name) getOrElse |
|
1209 Export.empty_entry(session, theory_name, name) |
|
1210 |
|
1211 override def toString: String = |
|
1212 { |
|
1213 val s = |
|
1214 database_server match { |
|
1215 case Some(db) => db.toString |
|
1216 case None => "input_dirs = " + store.input_dirs.map(_.absolute).mkString(", ") |
|
1217 } |
|
1218 "Database_Context(" + s + ")" |
|
1219 } |
|
1220 } |
|
1221 |
1183 def store(options: Options): Store = new Store(options) |
1222 def store(options: Options): Store = new Store(options) |
1184 |
1223 |
1185 class Store private[Sessions](val options: Options) |
1224 class Store private[Sessions](val options: Options) |
1186 { |
1225 { |
1187 store => |
1226 store => |
1256 SSH.open_session(options, |
1295 SSH.open_session(options, |
1257 host = ssh_host, |
1296 host = ssh_host, |
1258 user = options.string("build_database_ssh_user"), |
1297 user = options.string("build_database_ssh_user"), |
1259 port = options.int("build_database_ssh_port"))), |
1298 port = options.int("build_database_ssh_port"))), |
1260 ssh_close = true) |
1299 ssh_close = true) |
|
1300 |
|
1301 def open_database_context(sessions_structure: Sessions.Structure): Database_Context = |
|
1302 new Database_Context(store, sessions_structure, |
|
1303 if (database_server) Some(open_database_server()) else None) |
1261 |
1304 |
1262 def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = |
1305 def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] = |
1263 { |
1306 { |
1264 def check(db: SQL.Database): Option[SQL.Database] = |
1307 def check(db: SQL.Database): Option[SQL.Database] = |
1265 if (output || session_info_exists(db)) Some(db) else { db.close; None } |
1308 if (output || session_info_exists(db)) Some(db) else { db.close; None } |