123 (seen ++ thys, (session, thys) :: batches) |
123 (seen ++ thys, (session, thys) :: batches) |
124 })._2 |
124 })._2 |
125 val theory_node_info = |
125 val theory_node_info = |
126 Par_List.map[Batch, List[(String, Node_Info)]]( |
126 Par_List.map[Batch, List[(String, Node_Info)]]( |
127 { case (session, thys) => |
127 { case (session, thys) => |
128 for (thy_name <- thys) yield { |
128 db_context.input_database(session) { (db, _) => |
129 val theory = |
129 val provider0 = Export.Provider.database(db, db_context.cache, session, "") |
130 if (thy_name == Thy_Header.PURE) Export_Theory.no_theory |
130 val result = |
131 else { |
131 for (thy_name <- thys) yield { |
132 val provider = Export.Provider.database_context(db_context, List(session), thy_name) |
132 val theory = |
133 if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) { |
133 if (thy_name == Thy_Header.PURE) Export_Theory.no_theory |
134 Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache) |
134 else { |
135 } |
135 val provider = provider0.focus(thy_name) |
136 else Export_Theory.no_theory |
136 if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) { |
|
137 Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache) |
|
138 } |
|
139 else Export_Theory.no_theory |
|
140 } |
|
141 thy_name -> Node_Info.make(theory) |
137 } |
142 } |
138 thy_name -> Node_Info.make(theory) |
143 Some(result) |
139 } |
144 } getOrElse Nil |
140 }, batches).flatten.toMap |
145 }, batches).flatten.toMap |
141 new Nodes(theory_node_info) |
146 new Nodes(theory_node_info) |
142 } |
147 } |
143 } |
148 } |
144 |
149 |