1215 case None => None |
1215 case None => None |
1216 } |
1216 } |
1217 } |
1217 } |
1218 |
1218 |
1219 def read_export( |
1219 def read_export( |
1220 sessions: List[String], |
1220 session_hierarchy: List[String], theory: String, name: String |
1221 theory_name: String, |
|
1222 name: String |
|
1223 ): Option[Export.Entry] = { |
1221 ): Option[Export.Entry] = { |
|
1222 def read(db: SQL.Database, session: String): Option[Export.Entry] = |
|
1223 Export.Entry_Name(session = session, theory = theory, name = name).read(db, store.cache) |
1224 val attempts = |
1224 val attempts = |
1225 database_server match { |
1225 database_server match { |
1226 case Some(db) => |
1226 case Some(db) => session_hierarchy.view.map(read(db, _)) |
1227 sessions.view.map(session_name => |
|
1228 Export.Entry_Name(session = session_name, theory = theory_name, name = name) |
|
1229 .read(db, store.cache)) |
|
1230 case None => |
1227 case None => |
1231 sessions.view.map(session_name => |
1228 session_hierarchy.view.map(session => |
1232 store.try_open_database(session_name) match { |
1229 store.try_open_database(session) match { |
1233 case Some(db) => |
1230 case Some(db) => using(db) { _ => read(db, session) } |
1234 using(db) { _ => |
|
1235 Export.Entry_Name(session = session_name, theory = theory_name, name = name) |
|
1236 .read(db, store.cache) } |
|
1237 case None => None |
1231 case None => None |
1238 }) |
1232 }) |
1239 } |
1233 } |
1240 attempts.collectFirst({ case Some(entry) => entry }) |
1234 attempts.collectFirst({ case Some(entry) => entry }) |
1241 } |
1235 } |
1242 |
1236 |
1243 def get_export( |
1237 def get_export(session_hierarchy: List[String], theory: String, name: String): Export.Entry = |
1244 session_hierarchy: List[String], theory_name: String, name: String): Export.Entry = |
1238 read_export(session_hierarchy, theory, name) getOrElse |
1245 read_export(session_hierarchy, theory_name, name) getOrElse |
1239 Export.empty_entry(theory, name) |
1246 Export.empty_entry(theory_name, name) |
|
1247 |
1240 |
1248 def get_classpath(structure: Structure, session: String): List[File.Content_Bytes] = |
1241 def get_classpath(structure: Structure, session: String): List[File.Content_Bytes] = |
1249 { |
1242 { |
1250 (for { |
1243 (for { |
1251 name <- structure.build_requirements(List(session)) |
1244 name <- structure.build_requirements(List(session)) |