equal
deleted
inserted
replaced
40 } |
40 } |
41 |
41 |
42 def component_sessions(): List[List[String]] = |
42 def component_sessions(): List[List[String]] = |
43 { |
43 { |
44 val toplevel_sessions = |
44 val toplevel_sessions = |
45 system.components().map(system.platform_file(_)).filter(is_session_dir) |
45 system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir) |
46 ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse |
46 ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse |
47 } |
47 } |
48 } |
48 } |