src/Pure/Thy/sessions.scala
changeset 73310 6e155bb1516d
parent 73042 22f5a6283477
child 73311 54262af6d310
equal deleted inserted replaced
73309:606ae85b8c6b 73310:6e155bb1516d
  1011   private def is_session_dir(dir: Path): Boolean =
  1011   private def is_session_dir(dir: Path): Boolean =
  1012     (dir + ROOT).is_file || (dir + ROOTS).is_file
  1012     (dir + ROOT).is_file || (dir + ROOTS).is_file
  1013 
  1013 
  1014   private def check_session_dir(dir: Path): Path =
  1014   private def check_session_dir(dir: Path): Path =
  1015     if (is_session_dir(dir)) File.pwd() + dir.expand
  1015     if (is_session_dir(dir)) File.pwd() + dir.expand
  1016     else error("Bad session root directory: " + dir.toString)
  1016     else error("Bad session root directory: " + dir.expand.toString)
  1017 
  1017 
  1018   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
  1018   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
  1019   {
  1019   {
  1020     val default_dirs = Isabelle_System.components().filter(is_session_dir)
  1020     val default_dirs = Isabelle_System.components().filter(is_session_dir)
  1021     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
  1021     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }