# HG changeset patch
# User wenzelm
# Date 1458132420 -3600
# Node ID 4854a38061de6830e04072dd16684f3c99f1861b
# Parent  aa3b47b321004cb0e1fa6c53cc6bb062424ecf48
tuned signature;

diff -r aa3b47b32100 -r 4854a38061de src/Pure/PIDE/batch_session.scala
--- 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))
diff -r aa3b47b32100 -r 4854a38061de src/Pure/Thy/sessions.scala
--- 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)
   }
 
diff -r aa3b47b32100 -r 4854a38061de src/Pure/Tools/build.scala
--- 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)
diff -r aa3b47b32100 -r 4854a38061de src/Pure/Tools/build_doc.scala
--- 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)
diff -r aa3b47b32100 -r 4854a38061de src/Tools/jEdit/src/isabelle_logic.scala
--- 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