author | wenzelm |
Mon, 10 Oct 2016 14:45:32 +0200 | |
changeset 64131 | f01fca58e0a5 |
parent 64130 | e17c211a0bb6 |
child 64132 | c2594513687b |
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 |
||
64131 | 10 |
import java.io.{InputStream, OutputStream} |
11 |
||
12 |
import scala.collection.JavaConversions |
|
13 |
||
64123 | 14 |
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, |
64130 | 15 |
OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp} |
64123 | 16 |
|
17 |
||
18 |
object SSH |
|
19 |
{ |
|
20 |
/* init */ |
|
21 |
||
64130 | 22 |
def init(options: Options): SSH = |
64123 | 23 |
{ |
64130 | 24 |
val config_dir = Path.explode(options.string("ssh_config_dir")) |
64123 | 25 |
if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) |
26 |
||
27 |
val jsch = new JSch |
|
28 |
||
64130 | 29 |
val config_file = Path.explode(options.string("ssh_config_file")) |
64123 | 30 |
if (config_file.is_file) |
31 |
jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) |
|
32 |
||
33 |
val known_hosts = config_dir + Path.explode("known_hosts") |
|
34 |
if (!known_hosts.is_file) known_hosts.file.createNewFile |
|
35 |
jsch.setKnownHosts(File.platform_path(known_hosts)) |
|
36 |
||
64130 | 37 |
val identity_files = |
38 |
Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_)) |
|
64123 | 39 |
for (identity_file <- identity_files if identity_file.is_file) |
40 |
jsch.addIdentity(File.platform_path(identity_file)) |
|
41 |
||
64130 | 42 |
new SSH(options, jsch) |
64123 | 43 |
} |
44 |
||
64130 | 45 |
def connect_timeout(options: Options): Int = |
46 |
options.seconds("ssh_connect_timeout").ms.toInt |
|
47 |
||
64123 | 48 |
|
49 |
/* logging */ |
|
50 |
||
51 |
def logging(verbose: Boolean = true, debug: Boolean = false) |
|
52 |
{ |
|
53 |
JSch.setLogger(if (verbose) new Logger(debug) else null) |
|
54 |
} |
|
55 |
||
56 |
private class Logger(debug: Boolean) extends JSch_Logger |
|
57 |
{ |
|
58 |
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug |
|
59 |
||
60 |
def log(level: Int, msg: String) |
|
61 |
{ |
|
62 |
level match { |
|
63 |
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) |
|
64 |
case JSch_Logger.WARN => Output.warning(msg) |
|
65 |
case _ => Output.writeln(msg) |
|
66 |
} |
|
67 |
} |
|
68 |
} |
|
69 |
||
70 |
||
64128 | 71 |
/* user info */ |
72 |
||
73 |
object No_User_Info extends UserInfo |
|
74 |
{ |
|
75 |
def getPassphrase: String = null |
|
76 |
def getPassword: String = null |
|
77 |
def promptPassword(msg: String): Boolean = false |
|
78 |
def promptPassphrase(msg: String): Boolean = false |
|
79 |
def promptYesNo(msg: String): Boolean = false |
|
80 |
def showMessage(msg: String): Unit = Output.writeln(msg) |
|
81 |
} |
|
82 |
||
83 |
||
64130 | 84 |
/* channel: exec, sftp etc. */ |
64129 | 85 |
|
64130 | 86 |
class Channel[C <: JSch_Channel] private[SSH](val session: Session, |
87 |
val kind: String, val channel_options: Options, val channel: C) |
|
64129 | 88 |
{ |
64130 | 89 |
override def toString: String = kind + " " + session.toString |
64129 | 90 |
|
91 |
def close { channel.disconnect } |
|
92 |
} |
|
93 |
||
64131 | 94 |
class Exec private[SSH]( |
95 |
session: Session, kind: String, channel_options: Options, channel: ChannelExec) |
|
96 |
extends Channel[ChannelExec](session, kind, channel_options, channel) |
|
97 |
{ |
|
98 |
def kill(signal: String) { channel.sendSignal(signal) } |
|
99 |
} |
|
100 |
||
101 |
||
102 |
class Sftp private[SSH]( |
|
103 |
session: Session, kind: String, channel_options: Options, channel: ChannelSftp) |
|
104 |
extends Channel[ChannelSftp](session, kind, channel_options, channel) |
|
105 |
{ |
|
106 |
def home: String = channel.getHome() |
|
107 |
||
108 |
def chmod(permissions: Int, remote_path: String) { channel.chmod(permissions, remote_path) } |
|
109 |
def mv(remote_path1: String, remote_path2: String): Unit = |
|
110 |
channel.rename(remote_path1, remote_path2) |
|
111 |
def rm(remote_path: String) { channel.rm(remote_path) } |
|
112 |
def mkdir(remote_path: String) { channel.mkdir(remote_path) } |
|
113 |
def rmdir(remote_path: String) { channel.rmdir(remote_path) } |
|
114 |
||
115 |
def open_input(remote_path: String): InputStream = channel.get(remote_path) |
|
116 |
def open_output(remote_path: String): OutputStream = channel.put(remote_path) |
|
117 |
||
118 |
def read_file(remote_path: String, local_path: Path): Unit = |
|
119 |
channel.get(remote_path, File.platform_path(local_path)) |
|
120 |
def read_bytes(remote_path: String): Bytes = |
|
121 |
using(open_input(remote_path))(Bytes.read_stream(_)) |
|
122 |
def read(remote_path: String): String = |
|
123 |
using(open_input(remote_path))(File.read_stream(_)) |
|
124 |
||
125 |
def write_file(remote_path: String, local_path: Path): Unit = |
|
126 |
channel.put(File.platform_path(local_path), remote_path) |
|
127 |
def write_bytes(remote_path: String, bytes: Bytes): Unit = |
|
128 |
using(open_output(remote_path))(bytes.write_stream(_)) |
|
129 |
def write(remote_path: String, text: String): Unit = |
|
130 |
using(open_output(remote_path))(stream => Bytes(text).write_stream(stream)) |
|
131 |
} |
|
132 |
||
64129 | 133 |
|
64123 | 134 |
/* session */ |
135 |
||
64130 | 136 |
class Session private[SSH](val session_options: Options, val session: JSch_Session) |
64123 | 137 |
{ |
138 |
override def toString: String = |
|
139 |
(if (session.getUserName == null) "" else session.getUserName + "@") + |
|
140 |
(if (session.getHost == null) "" else session.getHost) + |
|
64126 | 141 |
(if (session.getPort == 22) "" else ":" + session.getPort) + |
142 |
(if (session.isConnected) "" else " (disconnected)") |
|
64123 | 143 |
|
64126 | 144 |
def close { session.disconnect } |
64123 | 145 |
|
64131 | 146 |
def exec(command: String, options: Options = session_options): Exec = |
64129 | 147 |
{ |
64130 | 148 |
val kind = "exec" |
149 |
val channel = session.openChannel(kind).asInstanceOf[ChannelExec] |
|
64129 | 150 |
channel.setCommand(command) |
151 |
||
64130 | 152 |
channel.connect(connect_timeout(options)) |
64131 | 153 |
new Exec(this, kind, options, channel) |
64129 | 154 |
} |
64123 | 155 |
|
64131 | 156 |
def sftp(options: Options = session_options): Sftp = |
64130 | 157 |
{ |
158 |
val kind = "sftp" |
|
159 |
val channel = session.openChannel(kind).asInstanceOf[ChannelSftp] |
|
160 |
||
161 |
channel.connect(connect_timeout(options)) |
|
64131 | 162 |
new Sftp(this, kind, options, channel) |
64130 | 163 |
} |
64123 | 164 |
} |
165 |
} |
|
166 |
||
64130 | 167 |
class SSH private(val options: Options, val jsch: JSch) |
64123 | 168 |
{ |
64130 | 169 |
def open_session(host: String, port: Int = 22, user: String = null): SSH.Session = |
64123 | 170 |
{ |
171 |
val session = jsch.getSession(user, host, port) |
|
64125
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
172 |
|
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
173 |
session.setUserInfo(SSH.No_User_Info) |
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
174 |
session.setConfig("MaxAuthTries", "3") |
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
175 |
|
64130 | 176 |
if (options.bool("ssh_compression")) { |
64123 | 177 |
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") |
178 |
session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") |
|
179 |
session.setConfig("compression_level", "9") |
|
180 |
} |
|
64125
a034dac5ca3c
clarified (hardwired!) default (see also jEdit/FTP);
wenzelm
parents:
64124
diff
changeset
|
181 |
|
64130 | 182 |
session.connect(SSH.connect_timeout(options)) |
183 |
new SSH.Session(options, session) |
|
64123 | 184 |
} |
185 |
} |