# HG changeset patch
# User wenzelm
# Date 1510069826 -3600
# Node ID 687c822ee5e36e0600ad51a0b498ae90ce65915a
# Parent  961285f581e6cf2141707234de74bd3b42694af2
tuned signature;

diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/Admin/afp.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -36,7 +36,7 @@
   val sessions: List[String] = entries.flatMap(_.sessions)
 
   val sessions_structure: Sessions.T =
-    Sessions.load(options, dirs = List(main_dir)).
+    Sessions.load_structure(options, dirs = List(main_dir)).
       selection(Sessions.Selection(sessions = sessions.toList))
 
 
diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/Admin/build_doc.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -22,7 +22,7 @@
     system_mode: Boolean = false,
     docs: List[String] = Nil): Int =
   {
-    val sessions_structure = Sessions.load(options)
+    val sessions_structure = Sessions.load_structure(options)
     val selection =
       for {
         name <- sessions_structure.build_topological_order
diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -33,7 +33,7 @@
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
         val selected_sessions =
-          sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
+          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
         selected_sessions.build_requirements(List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
       }
diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -345,7 +345,7 @@
     focus_session: Boolean = false,
     required_session: Boolean = false): Base_Info =
   {
-    val full_sessions = load(options, dirs = dirs)
+    val full_sessions = load_structure(options, dirs = dirs)
     val global_theories = full_sessions.global_theories
 
     val selected_sessions =
@@ -400,7 +400,7 @@
 
     val full_sessions1 =
       if (infos1.isEmpty) full_sessions
-      else load(options, dirs = dirs, infos = infos1)
+      else load_structure(options, dirs = dirs, infos = infos1)
 
     val select_sessions1 =
       if (focus_session) full_sessions1.imports_descendants(List(session1))
@@ -784,7 +784,7 @@
     (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   }
 
-  def load(options: Options,
+  def load_structure(options: Options,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Info] = Nil): T =
diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -382,7 +382,7 @@
     /* session selection and dependencies */
 
     val full_sessions =
-      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
+      Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
     def sources_stamp(deps: Sessions.Deps, name: String): String =
     {
diff -r 961285f581e6 -r 687c822ee5e3 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Pure/Tools/imports.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -99,7 +99,7 @@
     select_dirs: List[Path] = Nil,
     verbose: Boolean = false) =
   {
-    val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
+    val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
     val selected_sessions = full_sessions.selection(selection)
 
     val deps =
@@ -312,8 +312,8 @@
           verbose = verbose)
       }
       else if (operation_update && incremental_update) {
-        Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection).
-          imports_topological_order.foreach(name =>
+        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
+          selection(selection).imports_topological_order.foreach(name =>
             {
               imports(options, operation_update = operation_update, progress = progress,
                 update_message = " for session " + quote(name),
diff -r 961285f581e6 -r 687c822ee5e3 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 16:44:25 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 16:50:26 2017 +0100
@@ -45,7 +45,10 @@
   def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
 
   def logic_info(options: Options): Option[Sessions.Info] =
-    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
+    try {
+      Sessions.load_structure(session_options(options), dirs = session_dirs()).
+        get(logic_name(options))
+    }
     catch { case ERROR(_) => None }
 
   def logic_root(options: Options): Position.T =
@@ -68,7 +71,7 @@
 
     val session_list =
     {
-      val sessions_structure = Sessions.load(options.value, dirs = session_dirs())
+      val sessions_structure = Sessions.load_structure(options.value, dirs = session_dirs())
       val (main_sessions, other_sessions) =
         sessions_structure.imports_topological_order.
           partition(name => sessions_structure(name).groups.contains("main"))