115 def read( |
115 def read( |
116 presentation_sessions: List[String], |
116 presentation_sessions: List[String], |
117 deps: Sessions.Deps, |
117 deps: Sessions.Deps, |
118 db_context: Sessions.Database_Context |
118 db_context: Sessions.Database_Context |
119 ): Nodes = { |
119 ): Nodes = { |
|
120 val export_context = Export.context(db_context) |
|
121 |
120 type Batch = (String, List[String]) |
122 type Batch = (String, List[String]) |
121 val batches = |
123 val batches = |
122 presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))( |
124 presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))( |
123 { case ((seen, batches), session) => |
125 { case ((seen, batches), session) => |
124 val thys = deps(session).loaded_theories.keys.filterNot(seen) |
126 val thys = deps(session).loaded_theories.keys.filterNot(seen) |
125 (seen ++ thys, (session, thys) :: batches) |
127 (seen ++ thys, (session, thys) :: batches) |
126 })._2 |
128 })._2 |
|
129 |
127 val theory_node_info = |
130 val theory_node_info = |
128 Par_List.map[Batch, List[(String, Node_Info)]]( |
131 Par_List.map[Batch, List[(String, Node_Info)]]( |
129 { case (session, thys) => |
132 { case (session, thys) => |
130 db_context.database(session) { db => |
133 using(export_context.open_session(deps.base_info(session))) { session_context => |
131 val provider = Export.Provider.database(db, db_context.cache, session) |
134 for (thy_name <- thys) yield { |
132 val result = |
135 val theory_context = session_context.theory(thy_name) |
133 for (thy_name <- thys) yield { |
136 val theory = |
134 val theory = |
137 Export_Theory.read_theory(theory_context, |
135 if (thy_name == Thy_Header.PURE) Export_Theory.no_theory |
138 permissive = true, cache = db_context.cache) |
136 else { |
139 thy_name -> Node_Info.make(theory) |
137 Export_Theory.read_theory(provider, session, thy_name, |
140 } |
138 permissive = true, cache = db_context.cache) |
141 } |
139 } |
|
140 thy_name -> Node_Info.make(theory) |
|
141 } |
|
142 Some(result) |
|
143 } getOrElse Nil |
|
144 }, batches).flatten.toMap |
142 }, batches).flatten.toMap |
|
143 |
145 val files_info = |
144 val files_info = |
146 deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session => |
145 deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session => |
147 db_context.database(session) { db => |
146 using(export_context.open_session(deps.base_info(session))) { session_context => |
148 val res = |
147 session_context.theory_names().flatMap { theory => |
149 Export.read_theory_names(db, session).flatMap { theory => |
148 val theory_context = session_context.theory(theory) |
150 val files = |
149 Export.read_files(theory_context(_, permissive = true)) match { |
151 Export.read_files(name => |
150 case None => Nil |
152 Export.Entry_Name(session = session, theory = theory, name = name) |
151 case Some((thy, other)) => |
153 .read(db, db_context.cache) |
152 val thy_file_info = File_Info(theory, is_theory = true) |
154 .getOrElse(Export.empty_entry(theory, name))) |
153 (thy -> thy_file_info) :: other.map(_ -> File_Info(theory)) |
155 files match { |
|
156 case None => Nil |
|
157 case Some((thy, other)) => |
|
158 val thy_file_info = File_Info(theory, is_theory = true) |
|
159 (thy -> thy_file_info) :: other.map(_ -> File_Info(theory)) |
|
160 } |
|
161 } |
154 } |
162 Some(res) |
155 } |
163 }.getOrElse(Nil)).toMap |
156 }).toMap |
|
157 |
164 new Nodes(theory_node_info, files_info) |
158 new Nodes(theory_node_info, files_info) |
165 } |
159 } |
166 } |
160 } |
167 |
161 |
168 class Nodes private( |
162 class Nodes private( |