# HG changeset patch # User wenzelm # Date 1570364278 -7200 # Node ID b254a95b6e771a2cd7e777b2122b4d4df8bf8635 # Parent 15656ad28691822aad11de60d52570f936c87eba tuned signature; diff -r 15656ad28691 -r b254a95b6e77 src/Pure/ML/ml_process.scala --- 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))) } diff -r 15656ad28691 -r b254a95b6e77 src/Pure/Thy/sessions.scala --- 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(