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(