16 |
16 |
17 def start_session( |
17 def start_session( |
18 options: Options, |
18 options: Options, |
19 session_name: String, |
19 session_name: String, |
20 session_dirs: List[Path] = Nil, |
20 session_dirs: List[Path] = Nil, |
|
21 include_sessions: List[String] = Nil, |
21 session_base: Option[Sessions.Base] = None, |
22 session_base: Option[Sessions.Base] = None, |
22 print_mode: List[String] = Nil, |
23 print_mode: List[String] = Nil, |
23 progress: Progress = No_Progress, |
24 progress: Progress = No_Progress, |
24 log: Logger = No_Logger): Session = |
25 log: Logger = No_Logger): Session = |
25 { |
26 { |
26 val base = |
27 val base = |
27 session_base getOrElse |
28 session_base getOrElse |
28 Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base |
29 Sessions.base_info(options, session_name, include_sessions = include_sessions, |
|
30 progress = progress, dirs = session_dirs).check_base |
29 val resources = new Thy_Resources(base, log = log) |
31 val resources = new Thy_Resources(base, log = log) |
30 val session = new Session(session_name, options, resources) |
32 val session = new Session(session_name, options, resources) |
31 |
33 |
32 val session_error = Future.promise[String] |
34 val session_error = Future.promise[String] |
33 var session_phase: Session.Consumer[Session.Phase] = null |
35 var session_phase: Session.Consumer[Session.Phase] = null |