| changeset 65525 | 360063716c71 |
| parent 65524 | 0910f1733909 |
| child 65528 | d15d302da7f0 |
| 65524:0910f1733909 | 65525:360063716c71 |
|---|---|
308 } |
308 } |
309 |
309 |
310 object Selection |
310 object Selection |
311 { |
311 { |
312 val empty: Selection = Selection() |
312 val empty: Selection = Selection() |
313 val all: Selection = Selection(all_sessions = true) |
|
313 } |
314 } |
314 |
315 |
315 sealed case class Selection( |
316 sealed case class Selection( |
316 requirements: Boolean = false, |
317 requirements: Boolean = false, |
317 all_sessions: Boolean = false, |
318 all_sessions: Boolean = false, |