--- a/src/Pure/ML/ml_process.scala Tue Nov 10 12:45:20 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Tue Nov 10 12:48:56 2020 +0100
@@ -32,7 +32,7 @@
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- sessions_structure.selection(Sessions.Selection.session(logic_name)).
+ sessions_structure.selection(logic_name).
build_requirements(List(logic_name)).
map(a => File.platform_path(store.the_heap(a)))
}
--- a/src/Pure/Thy/sessions.scala Tue Nov 10 12:45:20 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Nov 10 12:48:56 2020 +0100
@@ -711,6 +711,8 @@
restrict(build_graph), restrict(imports_graph))
}
+ def selection(session: String): Structure = selection(Selection.session(session))
+
def selection_deps(
options: Options,
selection: Selection,