src/Pure/Thy/sessions.scala
changeset 66575 191048506504
parent 66573 a6401a6417cf
child 66604 1af360d1cad2
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Aug 31 17:31:56 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Aug 31 19:06:14 2017 +0200
     1.3 @@ -153,8 +153,7 @@
     1.4        verbose: Boolean = false,
     1.5        list_files: Boolean = false,
     1.6        check_keywords: Set[String] = Set.empty,
     1.7 -      global_theories: Map[String, String] = Map.empty,
     1.8 -      all_known: Boolean = false): Deps =
     1.9 +      global_theories: Map[String, String] = Map.empty): Deps =
    1.10    {
    1.11      val session_bases =
    1.12        (Map.empty[String, Base] /: sessions.imports_topological_order)({
    1.13 @@ -274,9 +273,7 @@
    1.14            }
    1.15        })
    1.16  
    1.17 -    Deps(session_bases,
    1.18 -      if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
    1.19 -      else Known.empty)
    1.20 +    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
    1.21    }
    1.22  
    1.23    def session_base_errors(
    1.24 @@ -287,18 +284,12 @@
    1.25    {
    1.26      val full_sessions = load(options, dirs = dirs)
    1.27      val global_theories = full_sessions.global_theories
    1.28 -    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
    1.29 +    val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.30  
    1.31 -    if (all_known) {
    1.32 -      val deps =
    1.33 -        Sessions.deps(full_sessions, global_theories = global_theories, all_known = all_known)
    1.34 -      (deps.errors, deps(session).copy(known = deps.all_known))
    1.35 -    }
    1.36 -    else {
    1.37 -      val deps =
    1.38 -        Sessions.deps(selected_sessions, global_theories = global_theories)
    1.39 -      (deps.errors, deps(session))
    1.40 -    }
    1.41 +    val sessions: T = if (all_known) full_sessions else selected_sessions
    1.42 +    val deps = Sessions.deps(sessions, global_theories = global_theories)
    1.43 +    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.44 +    (deps.errors, base)
    1.45    }
    1.46  
    1.47    def session_base(