src/Pure/Thy/sessions.scala
changeset 65561 741b1d3930c0
parent 65560 327842649e8d
child 65566 94c514ea2846
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Apr 23 18:12:42 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Apr 23 18:47:56 2017 +0200
     1.3 @@ -628,6 +628,12 @@
     1.4      if (is_session_dir(dir)) File.pwd() + dir.expand
     1.5      else error("Bad session root directory: " + dir.toString)
     1.6  
     1.7 +  def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
     1.8 +  {
     1.9 +    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
    1.10 +    (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    1.11 +  }
    1.12 +
    1.13    def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
    1.14    {
    1.15      def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
    1.16 @@ -655,11 +661,9 @@
    1.17        else Nil
    1.18      }
    1.19  
    1.20 -    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
    1.21 -
    1.22      make(
    1.23        for {
    1.24 -        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    1.25 +        (select, dir) <- directories(dirs, select_dirs)
    1.26          info <- load_dir(select, check_session_dir(dir))
    1.27        } yield info)
    1.28    }