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