89 val store = Sessions.store(options) |
89 val store = Sessions.store(options) |
90 val session = new Session(options, Resources.empty) |
90 val session = new Session(options, Resources.empty) |
91 |
91 |
92 using(Export.open_session_context0(store, session_name)) { session_context => |
92 using(Export.open_session_context0(store, session_name)) { session_context => |
93 val result = |
93 val result = |
94 session_context.db_context.database(session_name) { db => |
94 for { |
95 val theories = store.read_theories(db, session_name) |
95 db <- session_context.session_db() |
96 val errors = store.read_errors(db, session_name) |
96 theories = store.read_theories(db, session_name) |
97 store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) |
97 errors = store.read_errors(db, session_name) |
98 } |
98 info <- store.read_build(db, session_name) |
|
99 } yield (theories, errors, info.return_code) |
99 result match { |
100 result match { |
100 case None => error("Missing build database for session " + quote(session_name)) |
101 case None => error("Missing build database for session " + quote(session_name)) |
101 case Some((used_theories, errors, rc)) => |
102 case Some((used_theories, errors, rc)) => |
102 theories.filterNot(used_theories.toSet) match { |
103 theories.filterNot(used_theories.toSet) match { |
103 case Nil => |
104 case Nil => |