changeset 70788 | b254a95b6e77 |
parent 70740 | 525c18b8ed53 |
child 70796 | 2739631ac368 |
--- 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(