equal
deleted
inserted
replaced
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.expand.toString) |
1016 else error("Bad session root directory (missing ROOT or ROOTS): " + 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, _)) } |