equal
deleted
inserted
replaced
92 val store = Sessions.store(options) |
92 val store = Sessions.store(options) |
93 val session = new Session(options, Resources.empty) |
93 val session = new Session(options, Resources.empty) |
94 |
94 |
95 using(store.open_database_context()) { db_context => |
95 using(store.open_database_context()) { db_context => |
96 val result = |
96 val result = |
97 db_context.input_database(session_name) { (db, _) => |
97 db_context.input_database(session_name) { db => |
98 val theories = store.read_theories(db, session_name) |
98 val theories = store.read_theories(db, session_name) |
99 val errors = store.read_errors(db, session_name) |
99 val errors = store.read_errors(db, session_name) |
100 store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) |
100 store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) |
101 } |
101 } |
102 result match { |
102 result match { |