equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 import java.io.{File, FileFilter} |
10 import java.io.{File, FileFilter} |
11 |
11 |
12 |
12 |
13 class Session_Manager(system: Isabelle_System) |
13 class Session_Manager |
14 { |
14 { |
15 val ROOT_NAME = "session.root" |
15 val ROOT_NAME = "session.root" |
16 |
16 |
17 def is_session_file(file: File): Boolean = |
17 def is_session_file(file: File): Boolean = |
18 file.isFile && file.getName == ROOT_NAME |
18 file.isFile && file.getName == ROOT_NAME |
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(s => system.platform_file(Path.explode(s))).filter(is_session_dir) |
45 Isabelle_System.components().map(s => |
|
46 Isabelle_System.platform_file(Path.explode(s))).filter(is_session_dir) |
46 ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse |
47 ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse |
47 } |
48 } |
48 } |
49 } |