author | wenzelm |
Mon, 10 Oct 2016 10:41:04 +0200 | |
changeset 64127 | 14782d58a503 |
parent 64126 | 42bcd207598d |
child 64128 | cc5ea4d648d8 |
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 |
||
10 |
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, |
|
11 |
OpenSSHConfig, UserInfo, ChannelExec, ChannelSftp} |
|
12 |
||
13 |
||
14 |
object SSH |
|
15 |
{ |
|
16 |
/* init */ |
|
17 |
||
64126 | 18 |
def init(config_dir: Path = Path.explode("~/.ssh"), |
64123 | 19 |
config_file: Path = Path.explode("~/.ssh/config"), |
20 |
identity_files: List[Path] = |
|
21 |
List("~/.ssh/id_dsa", "~/.ssh/id_ecdsa", "~/.ssh/id_rsa").map(Path.explode(_))): SSH = |
|
22 |
{ |
|
23 |
if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) |
|
24 |
||
25 |
val jsch = new JSch |
|
26 |
||
27 |
if (config_file.is_file) |
|
28 |
jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) |
|
29 |
||
30 |
val known_hosts = config_dir + Path.explode("known_hosts") |
|
31 |
if (!known_hosts.is_file) known_hosts.file.createNewFile |
|
32 |
jsch.setKnownHosts(File.platform_path(known_hosts)) |
|
33 |
||
34 |
for (identity_file <- identity_files if identity_file.is_file) |
|
35 |
jsch.addIdentity(File.platform_path(identity_file)) |
|
36 |
||
37 |
new SSH(jsch) |
|
38 |
} |
|
39 |
||
40 |
||
41 |
/* logging */ |
|
42 |
||
43 |
def logging(verbose: Boolean = true, debug: Boolean = false) |
|
44 |
{ |
|
45 |
JSch.setLogger(if (verbose) new Logger(debug) else null) |
|
46 |
} |
|
47 |
||
48 |
private class Logger(debug: Boolean) extends JSch_Logger |
|
49 |
{ |
|
50 |
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug |
|
51 |
||
52 |
def log(level: Int, msg: String) |
|
53 |
{ |
|
54 |
level match { |
|
55 |
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) |
|
56 |
case JSch_Logger.WARN => Output.warning(msg) |
|
57 |
case _ => Output.writeln(msg) |
|
58 |
} |
|
59 |
} |
|
60 |
} |
|
61 |
||
62 |
||
63 |
/* session */ |
|
64 |
||
64126 | 65 |
class Session private[SSH](val session: JSch_Session) |
64123 | 66 |
{ |
67 |
override def toString: String = |
|
68 |
(if (session.getUserName == null) "" else session.getUserName + "@") + |
|
69 |
(if (session.getHost == null) "" else session.getHost) + |
|
64126 | 70 |
(if (session.getPort == 22) "" else ":" + session.getPort) + |
71 |
(if (session.isConnected) "" else " (disconnected)") |
|
64123 | 72 |
|
64126 | 73 |
def close { session.disconnect } |
64123 | 74 |
|
75 |
def channel_exec: ChannelExec = |
|
76 |
session.openChannel("exec").asInstanceOf[ChannelExec] |
|
77 |
||
78 |
def channel_sftp: ChannelSftp = |
|
79 |
session.openChannel("sftp").asInstanceOf[ChannelSftp] |
|
80 |
} |
|
81 |
||
82 |
object No_User_Info extends UserInfo |
|
83 |
{ |
|
84 |
def getPassphrase: String = null |
|
85 |
def getPassword: String = null |
|
86 |
def promptPassword(msg: String): Boolean = false |
|
87 |
def promptPassphrase(msg: String): Boolean = false |
|
88 |
def promptYesNo(msg: String): Boolean = false |
|
89 |
def showMessage(msg: String): Unit = Output.writeln(msg) |
|
90 |
} |
|
91 |
} |
|
92 |
||
93 |
class SSH private(val jsch: JSch) |
|
94 |
{ |
|
64126 | 95 |
def open_session(host: String, port: Int = 22, user: String = null, |
64127
14782d58a503
more generous timeout default (see also jEdit/FTP);
wenzelm
parents:
64126
diff
changeset
|
96 |
connect_timeout: Time = Time.seconds(60), |
64126 | 97 |
compression: Boolean = true): SSH.Session = |
64123 | 98 |
{ |
99 |
val session = jsch.getSession(user, host, port) |
|
64125
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
100 |
|
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
101 |
session.setUserInfo(SSH.No_User_Info) |
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
102 |
session.setConfig("MaxAuthTries", "3") |
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
103 |
|
64123 | 104 |
if (compression) { |
105 |
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") |
|
106 |
session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") |
|
107 |
session.setConfig("compression_level", "9") |
|
108 |
} |
|
64125
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
109 |
|
64127
14782d58a503
more generous timeout default (see also jEdit/FTP);
wenzelm
parents:
64126
diff
changeset
|
110 |
if (connect_timeout.is_zero) session.connect |
14782d58a503
more generous timeout default (see also jEdit/FTP);
wenzelm
parents:
64126
diff
changeset
|
111 |
else session.connect(connect_timeout.ms.toInt) |
14782d58a503
more generous timeout default (see also jEdit/FTP);
wenzelm
parents:
64126
diff
changeset
|
112 |
|
64126 | 113 |
new SSH.Session(session) |
64123 | 114 |
} |
115 |
} |