equal
deleted
inserted
replaced
180 |
180 |
181 def get_imports: Base = |
181 def get_imports: Base = |
182 imports getOrElse Base.bootstrap(session_directories, global_theories) |
182 imports getOrElse Base.bootstrap(session_directories, global_theories) |
183 } |
183 } |
184 |
184 |
185 sealed case class Deps( |
185 sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) |
186 sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known) |
|
187 { |
186 { |
188 override def toString: String = "Sessions.Deps(" + sessions_structure + ")" |
187 override def toString: String = "Sessions.Deps(" + sessions_structure + ")" |
189 |
188 |
190 def is_empty: Boolean = session_bases.isEmpty |
189 def is_empty: Boolean = session_bases.isEmpty |
191 def apply(name: String): Base = session_bases(name) |
190 def apply(name: String): Base = session_bases(name) |
427 cat_error(msg, "The error(s) above occurred in session " + |
426 cat_error(msg, "The error(s) above occurred in session " + |
428 quote(info.name) + Position.here(info.pos)) |
427 quote(info.name) + Position.here(info.pos)) |
429 } |
428 } |
430 }) |
429 }) |
431 |
430 |
432 val all_known = |
431 Deps(sessions_structure, session_bases) |
433 Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_))) |
|
434 |
|
435 Deps(sessions_structure, session_bases, all_known) |
|
436 } |
432 } |
437 |
433 |
438 |
434 |
439 /* base info */ |
435 /* base info */ |
440 |
436 |