src/Pure/Thy/sessions.scala
changeset 66963 1c3d0c12bb51
parent 66962 e1bde71bace6
child 66964 9f2de457b95e
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:15:49 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
     1.3 @@ -318,34 +318,33 @@
     1.4      Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
     1.5    }
     1.6  
     1.7 -  def session_base_errors(
     1.8 +
     1.9 +  /* base info */
    1.10 +
    1.11 +  sealed case class Base_Info(base: Base, errors: List[String])
    1.12 +  {
    1.13 +    def platform_path: Base_Info = copy(base = base.platform_path)
    1.14 +    def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
    1.15 +  }
    1.16 +
    1.17 +  def session_base_info(
    1.18      options: Options,
    1.19      session: String,
    1.20      dirs: List[Path] = Nil,
    1.21      inlined_files: Boolean = false,
    1.22 -    all_known: Boolean = false): (List[String], Base) =
    1.23 +    all_known: Boolean = false): Base_Info =
    1.24    {
    1.25      val full_sessions = load(options, dirs = dirs)
    1.26      val global_theories = full_sessions.global_theories
    1.27      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.28  
    1.29 -    val sessions: T = if (all_known) full_sessions else selected_sessions
    1.30 -    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    1.31 -    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.32 -    (deps.errors, base)
    1.33 -  }
    1.34 +    val deps =
    1.35 +      Sessions.deps(if (all_known) full_sessions else selected_sessions,
    1.36 +        global_theories, inlined_files = inlined_files)
    1.37  
    1.38 -  def session_base(
    1.39 -    options: Options,
    1.40 -    session: String,
    1.41 -    dirs: List[Path] = Nil,
    1.42 -    inlined_files: Boolean = false,
    1.43 -    all_known: Boolean = false): Base =
    1.44 -  {
    1.45 -    val (errs, base) =
    1.46 -      session_base_errors(options, session, dirs = dirs,
    1.47 -        inlined_files = inlined_files, all_known = all_known)
    1.48 -    if (errs.isEmpty) base else error(cat_lines(errs))
    1.49 +    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.50 +
    1.51 +    Base_Info(base, deps.errors)
    1.52    }
    1.53  
    1.54