150 |
150 |
151 sealed case class Deps(session_bases: Map[String, Base], all_known: Known) |
151 sealed case class Deps(session_bases: Map[String, Base], all_known: Known) |
152 { |
152 { |
153 def is_empty: Boolean = session_bases.isEmpty |
153 def is_empty: Boolean = session_bases.isEmpty |
154 def apply(name: String): Base = session_bases(name) |
154 def apply(name: String): Base = session_bases(name) |
|
155 def get(name: String): Option[Base] = session_bases.get(name) |
155 |
156 |
156 def imported_sources(name: String): List[SHA1.Digest] = |
157 def imported_sources(name: String): List[SHA1.Digest] = |
157 session_bases(name).imported_sources.map(_._2) |
158 session_bases(name).imported_sources.map(_._2) |
158 |
159 |
159 def sources(name: String): List[SHA1.Digest] = |
160 def sources(name: String): List[SHA1.Digest] = |
335 def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) |
336 def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) |
336 } |
337 } |
337 |
338 |
338 def base_info(options: Options, session: String, |
339 def base_info(options: Options, session: String, |
339 dirs: List[Path] = Nil, |
340 dirs: List[Path] = Nil, |
|
341 ancestor_session: Option[String] = None, |
340 all_known: Boolean = false, |
342 all_known: Boolean = false, |
341 focus_session: Boolean = false, |
343 focus_session: Boolean = false, |
342 required_session: Boolean = false): Base_Info = |
344 required_session: Boolean = false): Base_Info = |
343 { |
345 { |
344 val full_sessions = load(options, dirs = dirs) |
346 val full_sessions = load(options, dirs = dirs) |
345 val global_theories = full_sessions.global_theories |
347 val global_theories = full_sessions.global_theories |
346 |
348 |
347 val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2 |
349 val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2 |
348 val info = selected_sessions(session) |
350 val info = selected_sessions(session) |
|
351 val ancestor = ancestor_session orElse info.parent |
349 |
352 |
350 val (session1, infos1) = |
353 val (session1, infos1) = |
351 if (required_session && info.parent.isDefined) { |
354 if (required_session && ancestor.isDefined) { |
352 val deps = Sessions.deps(selected_sessions, global_theories) |
355 val deps = Sessions.deps(selected_sessions, global_theories) |
353 val base = deps(session) |
356 val base = deps(session) |
354 |
357 |
355 val parent_loaded = deps(info.parent.get).loaded_theories.defined(_) |
358 val ancestor_loaded = |
|
359 deps.get(ancestor.get) match { |
|
360 case None => |
|
361 error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session)) |
|
362 case Some(ancestor_base) => ancestor_base.loaded_theories.defined(_) |
|
363 } |
356 |
364 |
357 val required_theories = |
365 val required_theories = |
358 for { |
366 for { |
359 thy <- base.loaded_theories.keys |
367 thy <- base.loaded_theories.keys |
360 if !parent_loaded(thy) && base.theory_qualifier(thy) != session |
368 if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session |
361 } |
369 } |
362 yield thy |
370 yield thy |
363 |
371 |
364 if (required_theories.isEmpty) (info.parent.get, Nil) |
372 if (required_theories.isEmpty) (ancestor.get, Nil) |
365 else { |
373 else { |
366 val other_name = info.name + "(base)" |
374 val other_name = info.name + "_base(" + ancestor.get + ")" |
367 (other_name, |
375 (other_name, |
368 List( |
376 List( |
369 make_info(info.options, |
377 make_info(info.options, |
370 dir_selected = false, |
378 dir_selected = false, |
371 dir = info.dir, |
379 dir = info.dir, |
373 Session_Entry( |
381 Session_Entry( |
374 pos = info.pos, |
382 pos = info.pos, |
375 name = other_name, |
383 name = other_name, |
376 groups = info.groups, |
384 groups = info.groups, |
377 path = ".", |
385 path = ".", |
378 parent = info.parent, |
386 parent = ancestor, |
379 description = "Required theory imports from other sessions", |
387 description = "Required theory imports from other sessions", |
380 options = Nil, |
388 options = Nil, |
381 imports = info.imports, |
389 imports = info.imports, |
382 theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), |
390 theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), |
383 document_files = Nil)))) |
391 document_files = Nil)))) |