src/Pure/Thy/sessions.scala
changeset 66964 9f2de457b95e
parent 66963 1c3d0c12bb51
child 66965 9cec50354099
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 18:45:33 2017 +0100
     1.3 @@ -321,12 +321,6 @@
     1.4  
     1.5    /* base info */
     1.6  
     1.7 -  sealed case class Base_Info(base: Base, errors: List[String])
     1.8 -  {
     1.9 -    def platform_path: Base_Info = copy(base = base.platform_path)
    1.10 -    def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    1.11 -  }
    1.12 -
    1.13    def session_base_info(
    1.14      options: Options,
    1.15      session: String,
    1.16 @@ -338,13 +332,19 @@
    1.17      val global_theories = full_sessions.global_theories
    1.18      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.19  
    1.20 -    val deps =
    1.21 -      Sessions.deps(if (all_known) full_sessions else selected_sessions,
    1.22 -        global_theories, inlined_files = inlined_files)
    1.23 -
    1.24 +    val sessions: T = if (all_known) full_sessions else selected_sessions
    1.25 +    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    1.26      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.27  
    1.28 -    Base_Info(base, deps.errors)
    1.29 +    new Base_Info(sessions, deps, base)
    1.30 +  }
    1.31 +
    1.32 +  final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
    1.33 +  {
    1.34 +    def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
    1.35 +
    1.36 +    def errors: List[String] = deps.errors
    1.37 +    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    1.38    }
    1.39  
    1.40