--- a/src/Pure/PIDE/batch_session.scala Wed Mar 16 11:45:25 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala Wed Mar 16 13:47:00 2016 +0100
@@ -18,7 +18,7 @@
dirs: List[Path] = Nil,
session: String): Batch_Session =
{
- val (_, session_tree) = Sessions.find(options, dirs).selection(sessions = List(session))
+ val (_, session_tree) = Sessions.load(options, dirs).selection(sessions = List(session))
val session_info = session_tree(session)
val parent_session =
session_info.parent getOrElse error("No parent session for " + quote(session))
--- a/src/Pure/Thy/sessions.scala Wed Mar 16 11:45:25 2016 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Mar 16 13:47:00 2016 +0100
@@ -270,7 +270,7 @@
}
- /* find sessions within certain directories */
+ /* load sessions from certain directories */
private def is_session_dir(dir: Path): Boolean =
(dir + ROOT).is_file || (dir + ROOTS).is_file
@@ -279,15 +279,15 @@
if (is_session_dir(dir)) dir
else error("Bad session root directory: " + dir.toString)
- def find(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
+ def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
{
- def find_dir(select: Boolean, dir: Path): List[(String, Info)] =
- find_root(select, dir) ::: find_roots(select, dir)
+ def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
+ load_root(select, dir) ::: load_roots(select, dir)
- def find_root(select: Boolean, dir: Path): List[(String, Info)] =
+ def load_root(select: Boolean, dir: Path): List[(String, Info)] =
Parser.parse(options, select, dir)
- def find_roots(select: Boolean, dir: Path): List[(String, Info)] =
+ def load_roots(select: Boolean, dir: Path): List[(String, Info)] =
{
val roots = dir + ROOTS
if (roots.is_file) {
@@ -300,7 +300,7 @@
case ERROR(msg) =>
error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
}
- info <- find_dir(select, dir1)
+ info <- load_dir(select, dir1)
} yield info
}
else Nil
@@ -313,7 +313,7 @@
Tree(
for {
(select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
- info <- find_dir(select, dir)
+ info <- load_dir(select, dir)
} yield info)
}
--- a/src/Pure/Tools/build.scala Wed Mar 16 11:45:25 2016 +0100
+++ b/src/Pure/Tools/build.scala Wed Mar 16 13:47:00 2016 +0100
@@ -209,7 +209,7 @@
dirs: List[Path],
sessions: List[String]): Deps =
{
- val (_, tree) = Sessions.find(options, dirs = dirs).selection(sessions = sessions)
+ val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = sessions)
dependencies(inlined_files = inlined_files, tree = tree)
}
@@ -451,7 +451,7 @@
{
/* session tree and dependencies */
- val full_tree = Sessions.find(options.int("completion_limit") = 0, dirs, select_dirs)
+ val full_tree = Sessions.load(options.int("completion_limit") = 0, dirs, select_dirs)
val (selected, selected_tree) =
full_tree.selection(requirements, all_sessions,
exclude_session_groups, exclude_sessions, session_groups, sessions)
--- a/src/Pure/Tools/build_doc.scala Wed Mar 16 11:45:25 2016 +0100
+++ b/src/Pure/Tools/build_doc.scala Wed Mar 16 13:47:00 2016 +0100
@@ -24,7 +24,7 @@
{
val selection =
for {
- (name, info) <- Sessions.find(options).topological_order
+ (name, info) <- Sessions.load(options).topological_order
if info.groups.contains("doc")
doc = info.options.string("document_variants")
if all_docs || docs.contains(doc)
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 16 11:45:25 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Mar 16 13:47:00 2016 +0100
@@ -84,7 +84,7 @@
def session_list(): List[String] =
{
- val session_tree = Sessions.find(PIDE.options.value, dirs = session_dirs())
+ val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
val (main_sessions, other_sessions) =
session_tree.topological_order.partition(p => p._2.groups.contains("main"))
main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted