equal
deleted
inserted
replaced
111 |
111 |
112 object Nodes { |
112 object Nodes { |
113 val empty: Nodes = new Nodes(Map.empty, Map.empty) |
113 val empty: Nodes = new Nodes(Map.empty, Map.empty) |
114 |
114 |
115 def read( |
115 def read( |
116 export_context: Export.Context, |
116 database_context: Export.Database_Context, |
117 deps: Sessions.Deps, |
117 deps: Sessions.Deps, |
118 presentation_sessions: List[String] |
118 presentation_sessions: List[String] |
119 ): Nodes = { |
119 ): Nodes = { |
120 |
120 |
121 def open_session(session: String): Export.Session_Context = |
121 def open_session(session: String): Export.Session_Context = |
122 export_context.open_session(deps.base_info(session)) |
122 database_context.open_session(deps.base_info(session)) |
123 |
123 |
124 type Batch = (String, List[String]) |
124 type Batch = (String, List[String]) |
125 val batches = |
125 val batches = |
126 presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))( |
126 presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))( |
127 { case ((seen, batches), session) => |
127 { case ((seen, batches), session) => |