319 } |
319 } |
320 |
320 |
321 |
321 |
322 /* base info */ |
322 /* base info */ |
323 |
323 |
324 sealed case class Base_Info(base: Base, errors: List[String]) |
|
325 { |
|
326 def platform_path: Base_Info = copy(base = base.platform_path) |
|
327 def check: Base = if (errors.isEmpty) base else error(cat_lines(errors)) |
|
328 } |
|
329 |
|
330 def session_base_info( |
324 def session_base_info( |
331 options: Options, |
325 options: Options, |
332 session: String, |
326 session: String, |
333 dirs: List[Path] = Nil, |
327 dirs: List[Path] = Nil, |
334 inlined_files: Boolean = false, |
328 inlined_files: Boolean = false, |
336 { |
330 { |
337 val full_sessions = load(options, dirs = dirs) |
331 val full_sessions = load(options, dirs = dirs) |
338 val global_theories = full_sessions.global_theories |
332 val global_theories = full_sessions.global_theories |
339 val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session))) |
333 val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session))) |
340 |
334 |
341 val deps = |
335 val sessions: T = if (all_known) full_sessions else selected_sessions |
342 Sessions.deps(if (all_known) full_sessions else selected_sessions, |
336 val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files) |
343 global_theories, inlined_files = inlined_files) |
|
344 |
|
345 val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session) |
337 val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session) |
346 |
338 |
347 Base_Info(base, deps.errors) |
339 new Base_Info(sessions, deps, base) |
|
340 } |
|
341 |
|
342 final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base) |
|
343 { |
|
344 def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path) |
|
345 |
|
346 def errors: List[String] = deps.errors |
|
347 def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) |
348 } |
348 } |
349 |
349 |
350 |
350 |
351 /* cumulative session info */ |
351 /* cumulative session info */ |
352 |
352 |