author | wenzelm |
Tue, 11 Oct 2016 10:43:27 +0200 | |
changeset 64142 | 954451356017 |
parent 64141 | 79cd4be708fb |
child 64166 | 44925cf6ded1 |
permissions | -rw-r--r-- |
64123 | 1 |
/* Title: Pure/General/ssh.scala |
2 |
Author: Makarius |
|
3 |
||
64124 | 4 |
SSH client based on JSch (see also http://www.jcraft.com/jsch/examples). |
64123 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
10 |
import java.io.{InputStream, OutputStream, ByteArrayOutputStream} |
64131 | 11 |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
12 |
import scala.collection.{mutable, JavaConversions} |
64131 | 13 |
|
64123 | 14 |
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, |
64132 | 15 |
OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS} |
64123 | 16 |
|
17 |
||
18 |
object SSH |
|
19 |
{ |
|
64141 | 20 |
/* user@host syntax */ |
21 |
||
22 |
object User_Host |
|
23 |
{ |
|
24 |
val Pattern = "^([^@]+)@(.+)$".r |
|
25 |
||
26 |
def parse(s: String): (String, String) = |
|
27 |
s match { |
|
28 |
case Pattern(user, host) => (user, host) |
|
29 |
case _ => ("", s) |
|
30 |
} |
|
31 |
||
32 |
def unapplySeq(s: String): Option[List[String]] = |
|
33 |
{ |
|
34 |
val (user, host) = parse(s) |
|
35 |
Some(List(user, host)) |
|
36 |
} |
|
37 |
} |
|
38 |
||
64142 | 39 |
val default_port = 22 |
40 |
||
64141 | 41 |
|
64123 | 42 |
/* init */ |
43 |
||
64130 | 44 |
def init(options: Options): SSH = |
64123 | 45 |
{ |
64130 | 46 |
val config_dir = Path.explode(options.string("ssh_config_dir")) |
64123 | 47 |
if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) |
48 |
||
49 |
val jsch = new JSch |
|
50 |
||
64130 | 51 |
val config_file = Path.explode(options.string("ssh_config_file")) |
64123 | 52 |
if (config_file.is_file) |
53 |
jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) |
|
54 |
||
55 |
val known_hosts = config_dir + Path.explode("known_hosts") |
|
56 |
if (!known_hosts.is_file) known_hosts.file.createNewFile |
|
57 |
jsch.setKnownHosts(File.platform_path(known_hosts)) |
|
58 |
||
64130 | 59 |
val identity_files = |
60 |
Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_)) |
|
64123 | 61 |
for (identity_file <- identity_files if identity_file.is_file) |
62 |
jsch.addIdentity(File.platform_path(identity_file)) |
|
63 |
||
64130 | 64 |
new SSH(options, jsch) |
64123 | 65 |
} |
66 |
||
64130 | 67 |
def connect_timeout(options: Options): Int = |
68 |
options.seconds("ssh_connect_timeout").ms.toInt |
|
69 |
||
64123 | 70 |
|
71 |
/* logging */ |
|
72 |
||
73 |
def logging(verbose: Boolean = true, debug: Boolean = false) |
|
74 |
{ |
|
75 |
JSch.setLogger(if (verbose) new Logger(debug) else null) |
|
76 |
} |
|
77 |
||
78 |
private class Logger(debug: Boolean) extends JSch_Logger |
|
79 |
{ |
|
80 |
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug |
|
81 |
||
82 |
def log(level: Int, msg: String) |
|
83 |
{ |
|
84 |
level match { |
|
85 |
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) |
|
86 |
case JSch_Logger.WARN => Output.warning(msg) |
|
87 |
case _ => Output.writeln(msg) |
|
88 |
} |
|
89 |
} |
|
90 |
} |
|
91 |
||
92 |
||
64128 | 93 |
/* user info */ |
94 |
||
95 |
object No_User_Info extends UserInfo |
|
96 |
{ |
|
97 |
def getPassphrase: String = null |
|
98 |
def getPassword: String = null |
|
99 |
def promptPassword(msg: String): Boolean = false |
|
100 |
def promptPassphrase(msg: String): Boolean = false |
|
101 |
def promptYesNo(msg: String): Boolean = false |
|
102 |
def showMessage(msg: String): Unit = Output.writeln(msg) |
|
103 |
} |
|
104 |
||
105 |
||
64132 | 106 |
/* channel */ |
64129 | 107 |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
108 |
class Channel[C <: JSch_Channel] private[SSH]( |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
109 |
val session: Session, val kind: String, val options: Options, val channel: C) |
64129 | 110 |
{ |
64130 | 111 |
override def toString: String = kind + " " + session.toString |
64129 | 112 |
|
64142 | 113 |
def close() { channel.disconnect } |
64129 | 114 |
} |
115 |
||
64132 | 116 |
|
117 |
/* exec channel */ |
|
118 |
||
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
119 |
private val exec_wait_delay = Time.seconds(0.3) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
120 |
|
64131 | 121 |
class Exec private[SSH]( |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
122 |
session: Session, kind: String, options: Options, channel: ChannelExec) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
123 |
extends Channel[ChannelExec](session, kind, options, channel) |
64131 | 124 |
{ |
125 |
def kill(signal: String) { channel.sendSignal(signal) } |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
126 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
127 |
val exit_status: Future[Int] = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
128 |
Future.thread("ssh_wait") { |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
129 |
while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
130 |
channel.getExitStatus |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
131 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
132 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
133 |
val stdin: OutputStream = channel.getOutputStream |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
134 |
val stdout: InputStream = channel.getInputStream |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
135 |
val stderr: InputStream = channel.getErrStream |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
136 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
137 |
// after preparing streams |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
138 |
channel.connect(connect_timeout(options)) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
139 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
140 |
def result( |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
141 |
progress_stdout: String => Unit = (_: String) => (), |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
142 |
progress_stderr: String => Unit = (_: String) => (), |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
143 |
strict: Boolean = true): Process_Result = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
144 |
{ |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
145 |
stdin.close |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
146 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
147 |
def read_lines(stream: InputStream, progress: String => Unit): List[String] = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
148 |
{ |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
149 |
val result = new mutable.ListBuffer[String] |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
150 |
val line_buffer = new ByteArrayOutputStream(100) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
151 |
def line_flush() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
152 |
{ |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
153 |
val line = line_buffer.toString(UTF8.charset_name) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
154 |
progress(line) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
155 |
result += line |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
156 |
line_buffer.reset |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
157 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
158 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
159 |
var c = 0 |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
160 |
var finished = false |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
161 |
while (!finished) { |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
162 |
while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
163 |
if (c == 10) line_flush() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
164 |
else if (channel.isClosed) { |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
165 |
if (line_buffer.size > 0) line_flush() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
166 |
finished = true |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
167 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
168 |
else Thread.sleep(exec_wait_delay.ms) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
169 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
170 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
171 |
result.toList |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
172 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
173 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
174 |
val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) } |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
175 |
val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) } |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
176 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
177 |
def terminate() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
178 |
{ |
64136 | 179 |
close |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
180 |
out_lines.join |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
181 |
err_lines.join |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
182 |
exit_status.join |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
183 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
184 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
185 |
val rc = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
186 |
try { exit_status.join } |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
187 |
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
188 |
|
64136 | 189 |
close |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
190 |
if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
191 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
192 |
Process_Result(rc, out_lines.join, err_lines.join) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
193 |
} |
64131 | 194 |
} |
195 |
||
196 |
||
64132 | 197 |
/* Sftp channel */ |
198 |
||
199 |
type Attrs = SftpATTRS |
|
200 |
||
201 |
sealed case class Dir_Entry(name: String, attrs: Attrs) |
|
202 |
{ |
|
203 |
def is_file: Boolean = attrs.isReg |
|
204 |
def is_dir: Boolean = attrs.isDir |
|
205 |
} |
|
206 |
||
64131 | 207 |
class Sftp private[SSH]( |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
208 |
session: Session, kind: String, options: Options, channel: ChannelSftp) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
209 |
extends Channel[ChannelSftp](session, kind, options, channel) |
64131 | 210 |
{ |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
211 |
channel.connect(connect_timeout(options)) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
212 |
|
64131 | 213 |
def home: String = channel.getHome() |
214 |
||
215 |
def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) } |
|
216 |
def mv(remote_path1: String, remote_path2: String): Unit = |
|
217 |
channel.rename(remote_path1, remote_path2) |
|
218 |
def rm(remote_path: String) { channel.rm(remote_path) } |
|
219 |
def mkdir(remote_path: String) { channel.mkdir(remote_path) } |
|
220 |
def rmdir(remote_path: String) { channel.rmdir(remote_path) } |
|
221 |
||
64132 | 222 |
def stat(remote_path: String): Dir_Entry = |
223 |
Dir_Entry(remote_path, channel.stat(remote_path)) |
|
224 |
||
225 |
def read_dir(remote_path: String): List[Dir_Entry] = |
|
226 |
{ |
|
227 |
val dir = channel.ls(remote_path) |
|
228 |
(for { |
|
229 |
i <- (0 until dir.size).iterator |
|
230 |
a = dir.get(i).asInstanceOf[AnyRef] |
|
231 |
name = Untyped.get[String](a, "filename") |
|
232 |
attrs = Untyped.get[Attrs](a, "attrs") |
|
233 |
if name != "." && name != ".." |
|
234 |
} yield Dir_Entry(name, attrs)).toList |
|
235 |
} |
|
236 |
||
237 |
def find_files(remote_path: String, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = |
|
238 |
{ |
|
239 |
def find(dir: String): List[Dir_Entry] = |
|
240 |
read_dir(dir).flatMap(entry => |
|
241 |
{ |
|
242 |
val file = dir + "/" + entry.name |
|
64133 | 243 |
if (entry.is_dir) find(file) |
244 |
else if (pred(entry)) List(entry.copy(name = file)) |
|
245 |
else Nil |
|
64132 | 246 |
}) |
247 |
find(remote_path) |
|
248 |
} |
|
249 |
||
64131 | 250 |
def open_input(remote_path: String): InputStream = channel.get(remote_path) |
251 |
def open_output(remote_path: String): OutputStream = channel.put(remote_path) |
|
252 |
||
253 |
def read_file(remote_path: String, local_path: Path): Unit = |
|
254 |
channel.get(remote_path, File.platform_path(local_path)) |
|
255 |
def read_bytes(remote_path: String): Bytes = |
|
256 |
using(open_input(remote_path))(Bytes.read_stream(_)) |
|
257 |
def read(remote_path: String): String = |
|
258 |
using(open_input(remote_path))(File.read_stream(_)) |
|
259 |
||
260 |
def write_file(remote_path: String, local_path: Path): Unit = |
|
261 |
channel.put(File.platform_path(local_path), remote_path) |
|
262 |
def write_bytes(remote_path: String, bytes: Bytes): Unit = |
|
263 |
using(open_output(remote_path))(bytes.write_stream(_)) |
|
264 |
def write(remote_path: String, text: String): Unit = |
|
265 |
using(open_output(remote_path))(stream => Bytes(text).write_stream(stream)) |
|
266 |
} |
|
267 |
||
64129 | 268 |
|
64123 | 269 |
/* session */ |
270 |
||
64130 | 271 |
class Session private[SSH](val session_options: Options, val session: JSch_Session) |
64123 | 272 |
{ |
273 |
override def toString: String = |
|
274 |
(if (session.getUserName == null) "" else session.getUserName + "@") + |
|
275 |
(if (session.getHost == null) "" else session.getHost) + |
|
64142 | 276 |
(if (session.getPort == default_port) "" else ":" + session.getPort) + |
64126 | 277 |
(if (session.isConnected) "" else " (disconnected)") |
64123 | 278 |
|
64142 | 279 |
def close() { session.disconnect } |
64123 | 280 |
|
64135
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
281 |
def execute(command: String, |
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
282 |
options: Options = session_options, |
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
283 |
progress_stdout: String => Unit = (_: String) => (), |
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
284 |
progress_stderr: String => Unit = (_: String) => (), |
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
285 |
strict: Boolean = true): Process_Result = |
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
286 |
exec(command, options).result(progress_stdout, progress_stderr, strict) |
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
287 |
|
64131 | 288 |
def exec(command: String, options: Options = session_options): Exec = |
64129 | 289 |
{ |
64130 | 290 |
val kind = "exec" |
291 |
val channel = session.openChannel(kind).asInstanceOf[ChannelExec] |
|
64129 | 292 |
channel.setCommand(command) |
64131 | 293 |
new Exec(this, kind, options, channel) |
64129 | 294 |
} |
64123 | 295 |
|
64131 | 296 |
def sftp(options: Options = session_options): Sftp = |
64130 | 297 |
{ |
298 |
val kind = "sftp" |
|
299 |
val channel = session.openChannel(kind).asInstanceOf[ChannelSftp] |
|
64131 | 300 |
new Sftp(this, kind, options, channel) |
64130 | 301 |
} |
64137 | 302 |
|
303 |
||
304 |
/* tmp dirs */ |
|
305 |
||
306 |
def rm_tree(remote_dir: String): Unit = |
|
307 |
execute("rm -r -f " + File.bash_string(remote_dir)).check |
|
308 |
||
309 |
def tmp_dir(): String = |
|
310 |
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out |
|
311 |
||
312 |
def with_tmp_dir[A](body: String => A): A = |
|
313 |
{ |
|
314 |
val remote_dir = tmp_dir() |
|
315 |
try { body(remote_dir) } finally { rm_tree(remote_dir) } |
|
316 |
} |
|
64123 | 317 |
} |
318 |
} |
|
319 |
||
64130 | 320 |
class SSH private(val options: Options, val jsch: JSch) |
64123 | 321 |
{ |
64142 | 322 |
def open_session(host: String, port: Int = SSH.default_port, user: String = ""): SSH.Session = |
64123 | 323 |
{ |
64141 | 324 |
val session = jsch.getSession(if (user == "") null else user, host, port) |
64125
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
325 |
|
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
326 |
session.setUserInfo(SSH.No_User_Info) |
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
327 |
session.setConfig("MaxAuthTries", "3") |
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
328 |
|
64130 | 329 |
if (options.bool("ssh_compression")) { |
64123 | 330 |
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") |
331 |
session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") |
|
332 |
session.setConfig("compression_level", "9") |
|
333 |
} |
|
64125
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
334 |
|
64130 | 335 |
session.connect(SSH.connect_timeout(options)) |
336 |
new SSH.Session(options, session) |
|
64123 | 337 |
} |
338 |
} |