equal
deleted
inserted
replaced
28 |
28 |
29 def read_session( |
29 def read_session( |
30 store: Sessions.Store, |
30 store: Sessions.Store, |
31 sessions_structure: Sessions.Structure, |
31 sessions_structure: Sessions.Structure, |
32 session_name: String, |
32 session_name: String, |
33 progress: Progress = No_Progress, |
33 progress: Progress = new Progress, |
34 cache: Term.Cache = Term.make_cache()): Session = |
34 cache: Term.Cache = Term.make_cache()): Session = |
35 { |
35 { |
36 val thys = |
36 val thys = |
37 sessions_structure.build_requirements(List(session_name)).flatMap(session => |
37 sessions_structure.build_requirements(List(session_name)).flatMap(session => |
38 using(store.open_database(session))(db => |
38 using(store.open_database(session))(db => |