--- a/src/Pure/ML/ml_process.scala Sat Oct 05 15:34:54 2019 +0200
+++ b/src/Pure/ML/ml_process.scala Sun Oct 06 14:17:58 2019 +0200
@@ -35,8 +35,7 @@
val heaps: List[String] =
if (raw_ml_system) Nil
else {
- val selection = Sessions.Selection(sessions = List(logic_name))
- sessions_structure1.selection(selection).
+ sessions_structure1.selection(Sessions.Selection.session(logic_name)).
build_requirements(List(logic_name)).
map(a => File.platform_path(_store.the_heap(a)))
}
--- a/src/Pure/Thy/sessions.scala Sat Oct 05 15:34:54 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Oct 06 14:17:58 2019 +0200
@@ -547,6 +547,7 @@
{
val empty: Selection = Selection()
val all: Selection = Selection(all_sessions = true)
+ def session(session: String): Selection = Selection(sessions = List(session))
}
sealed case class Selection(