--- 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))
--- 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
--- 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)))
}
--- 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 =
--- 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 =
{
--- 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),
--- 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"))