src/Tools/jEdit/src/jedit_sessions.scala
changeset 67023 e27e05d6f2a7
parent 66989 25665e7775b7
child 67024 72d37a2e9cca
     1.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 11:11:37 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 15:45:33 2017 +0100
     1.3 @@ -68,10 +68,11 @@
     1.4  
     1.5      val session_list =
     1.6      {
     1.7 -      val sessions = Sessions.load(options.value, dirs = session_dirs())
     1.8 +      val sessions_structure = Sessions.load(options.value, dirs = session_dirs())
     1.9        val (main_sessions, other_sessions) =
    1.10 -        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
    1.11 -      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
    1.12 +        sessions_structure.imports_topological_order.
    1.13 +          partition(name => sessions_structure(name).groups.contains("main"))
    1.14 +      main_sessions.sorted ::: other_sessions.sorted
    1.15      }
    1.16  
    1.17      val entries =