112 } |
112 } |
113 |
113 |
114 |
114 |
115 /* remote sessions */ |
115 /* remote sessions */ |
116 |
116 |
117 def capture_open_session( |
117 object Session { |
118 options: Options, |
118 def open(options: Options, host: Host, progress: Progress = new Progress): Session = { |
119 host: Host, |
|
120 progress: Progress = new Progress |
|
121 ): Exn.Result[Session] = { |
|
122 progress.echo(host.message("connect ...")) |
|
123 try { |
|
124 val ssh_options = options ++ host.options |
119 val ssh_options = options ++ host.options |
125 val ssh = SSH.open_session(ssh_options, host.name, port = host.port, user = host.user) |
120 val ssh = SSH.open_session(ssh_options, host.name, port = host.port, user = host.user) |
126 Exn.Res[Session](new Session(host, ssh)) |
121 new Session(host, ssh, progress) |
127 } |
122 } |
128 catch { |
123 } |
129 case exn: Throwable => |
124 |
130 progress.echo_error_message(host.message("failed to connect\n" + Exn.message(exn))) |
125 final class Session private( |
131 Exn.Exn[Session](exn) |
126 val host: Host, |
132 } |
127 val ssh: SSH.Session, |
133 } |
128 val progress: Progress |
134 |
129 ) extends AutoCloseable { |
135 final class Session private[Build_Cluster](val host: Host, val ssh: SSH.Session) |
|
136 extends AutoCloseable { |
|
137 override def toString: String = ssh.toString |
130 override def toString: String = ssh.toString |
|
131 |
|
132 def options: Options = ssh.options |
138 |
133 |
139 def start(): Result = { |
134 def start(): Result = { |
140 val res = Process_Result.ok // FIXME |
135 val res = Process_Result.ok // FIXME |
141 Result(host, res) |
136 Result(host, res) |
142 } |
137 } |
166 |
161 |
167 def open(): Unit = synchronized { |
162 def open(): Unit = synchronized { |
168 require(_sessions.isEmpty) |
163 require(_sessions.isEmpty) |
169 |
164 |
170 val attempts = |
165 val attempts = |
171 Par_List.map( |
166 Par_List.map((host: Build_Cluster.Host) => |
172 Build_Cluster.capture_open_session(build_context.build_options, _, progress = progress), |
167 progress.capture( |
|
168 Build_Cluster.Session.open(build_context.build_options, host, progress = progress), |
|
169 msg = host.message("open ..."), |
|
170 err = exn => host.message("failed to open\n" + Exn.message(exn))), |
173 remote_hosts, thread = true) |
171 remote_hosts, thread = true) |
174 |
172 |
175 if (attempts.forall(Exn.the_res.isDefinedAt)) { |
173 if (attempts.forall(Exn.the_res.isDefinedAt)) { |
176 _sessions = attempts.map(Exn.the_res) |
174 _sessions = attempts.map(Exn.the_res) |
177 } |
175 } |