src/Pure/Thy/sessions.scala
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(