src/Pure/Thy/sessions.scala
changeset 66987 352b23c97ac8
parent 66984 a1d3e5df0c95
child 66988 7f8c1dd7576a
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Nov 01 22:13:38 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Nov 02 10:16:22 2017 +0100
     1.3 @@ -338,6 +338,7 @@
     1.4    def base_info(options: Options, session: String,
     1.5      dirs: List[Path] = Nil,
     1.6      all_known: Boolean = false,
     1.7 +    focus_session: Boolean = false,
     1.8      required_session: Boolean = false): Base_Info =
     1.9    {
    1.10      val full_sessions = load(options, dirs = dirs)
    1.11 @@ -387,7 +388,12 @@
    1.12      val full_sessions1 =
    1.13        if (infos1.isEmpty) full_sessions
    1.14        else load(options, dirs = dirs, infos = infos1)
    1.15 -    val selected_sessions1 = full_sessions1.selection(Selection(sessions = List(session1)))._2
    1.16 +
    1.17 +    val select_sessions1 =
    1.18 +      if (focus_session) full_sessions1.imports_descendants(List(session1))
    1.19 +      else List(session1)
    1.20 +    val selected_sessions1 =
    1.21 +      full_sessions1.selection(Selection(sessions = select_sessions1))._2
    1.22  
    1.23      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    1.24      val deps1 = Sessions.deps(sessions1, global_theories)