equal
deleted
inserted
replaced
79 val (main_sessions, other_sessions) = |
79 val (main_sessions, other_sessions) = |
80 session_tree.topological_order.partition(p => p._2.groups.contains("main")) |
80 session_tree.topological_order.partition(p => p._2.groups.contains("main")) |
81 main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted |
81 main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted |
82 } |
82 } |
83 |
83 |
84 def session_base(options: Options): Sessions.Base = |
|
85 { |
|
86 val base = |
|
87 try { Sessions.session_base(options, session_name(options), session_dirs()) } |
|
88 catch { case ERROR(_) => Sessions.pure_base(options) } |
|
89 base.copy(known_theories = |
|
90 for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_)))) |
|
91 } |
|
92 |
|
93 |
84 |
94 /* logic selector */ |
85 /* logic selector */ |
95 |
86 |
96 private class Logic_Entry(val name: String, val description: String) |
87 private class Logic_Entry(val name: String, val description: String) |
97 { |
88 { |