author | wenzelm |
Thu, 27 Apr 2017 15:56:55 +0200 | |
changeset 65594 | 659305708959 |
parent 65010 | a27e9908dcf7 |
child 65636 | df804cdba5f9 |
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 |
|
64222 | 14 |
import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException, |
64132 | 15 |
OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS} |
64123 | 16 |
|
17 |
||
18 |
object SSH |
|
19 |
{ |
|
64185 | 20 |
/* target machine: user@host syntax */ |
64141 | 21 |
|
64185 | 22 |
object Target |
64141 | 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]] = |
|
64185 | 33 |
parse(s) match { |
34 |
case (_, "") => None |
|
35 |
case (user, host) => Some(List(user, host)) |
|
36 |
} |
|
64141 | 37 |
} |
38 |
||
64142 | 39 |
val default_port = 22 |
40 |
||
64257 | 41 |
def connect_timeout(options: Options): Int = |
42 |
options.seconds("ssh_connect_timeout").ms.toInt |
|
64141 | 43 |
|
64325 | 44 |
def alive_interval(options: Options): Int = |
45 |
options.seconds("ssh_alive_interval").ms.toInt |
|
46 |
||
64123 | 47 |
|
64257 | 48 |
/* init context */ |
49 |
||
50 |
def init_context(options: Options): Context = |
|
64123 | 51 |
{ |
64130 | 52 |
val config_dir = Path.explode(options.string("ssh_config_dir")) |
64123 | 53 |
if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) |
54 |
||
55 |
val jsch = new JSch |
|
56 |
||
64130 | 57 |
val config_file = Path.explode(options.string("ssh_config_file")) |
64123 | 58 |
if (config_file.is_file) |
59 |
jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) |
|
60 |
||
61 |
val known_hosts = config_dir + Path.explode("known_hosts") |
|
62 |
if (!known_hosts.is_file) known_hosts.file.createNewFile |
|
63 |
jsch.setKnownHosts(File.platform_path(known_hosts)) |
|
64 |
||
64130 | 65 |
val identity_files = |
66 |
Library.space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_)) |
|
64123 | 67 |
for (identity_file <- identity_files if identity_file.is_file) |
68 |
jsch.addIdentity(File.platform_path(identity_file)) |
|
69 |
||
64257 | 70 |
new Context(options, jsch) |
64123 | 71 |
} |
72 |
||
64257 | 73 |
class Context private[SSH](val options: Options, val jsch: JSch) |
74 |
{ |
|
75 |
def update_options(new_options: Options): Context = new Context(new_options, jsch) |
|
76 |
||
65594 | 77 |
def open_session(host: String, user: String = "", port: Int = 0): Session = |
64257 | 78 |
{ |
65594 | 79 |
val session = |
80 |
jsch.getSession(if (user == "") null else user, host, if (port > 0) port else default_port) |
|
64257 | 81 |
|
82 |
session.setUserInfo(No_User_Info) |
|
64325 | 83 |
session.setServerAliveInterval(alive_interval(options)) |
64257 | 84 |
session.setConfig("MaxAuthTries", "3") |
85 |
||
86 |
if (options.bool("ssh_compression")) { |
|
87 |
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") |
|
88 |
session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") |
|
89 |
session.setConfig("compression_level", "9") |
|
90 |
} |
|
91 |
||
92 |
session.connect(connect_timeout(options)) |
|
93 |
new Session(options, session) |
|
94 |
} |
|
95 |
} |
|
64130 | 96 |
|
64123 | 97 |
|
98 |
/* logging */ |
|
99 |
||
100 |
def logging(verbose: Boolean = true, debug: Boolean = false) |
|
101 |
{ |
|
102 |
JSch.setLogger(if (verbose) new Logger(debug) else null) |
|
103 |
} |
|
104 |
||
105 |
private class Logger(debug: Boolean) extends JSch_Logger |
|
106 |
{ |
|
107 |
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug |
|
108 |
||
109 |
def log(level: Int, msg: String) |
|
110 |
{ |
|
111 |
level match { |
|
112 |
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) |
|
113 |
case JSch_Logger.WARN => Output.warning(msg) |
|
114 |
case _ => Output.writeln(msg) |
|
115 |
} |
|
116 |
} |
|
117 |
} |
|
118 |
||
119 |
||
64128 | 120 |
/* user info */ |
121 |
||
122 |
object No_User_Info extends UserInfo |
|
123 |
{ |
|
124 |
def getPassphrase: String = null |
|
125 |
def getPassword: String = null |
|
126 |
def promptPassword(msg: String): Boolean = false |
|
127 |
def promptPassphrase(msg: String): Boolean = false |
|
128 |
def promptYesNo(msg: String): Boolean = false |
|
129 |
def showMessage(msg: String): Unit = Output.writeln(msg) |
|
130 |
} |
|
131 |
||
132 |
||
65009 | 133 |
/* port forwarding */ |
134 |
||
65010 | 135 |
object Port_Forwarding |
65009 | 136 |
{ |
65010 | 137 |
def open(ssh: Session, |
138 |
local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = |
|
139 |
{ |
|
140 |
val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) |
|
141 |
new Port_Forwarding(ssh, local_host, port, remote_host, remote_port) |
|
142 |
} |
|
143 |
} |
|
144 |
||
145 |
class Port_Forwarding private[SSH]( |
|
146 |
ssh: SSH.Session, |
|
147 |
val local_host: String, |
|
148 |
val local_port: Int, |
|
149 |
val remote_host: String, |
|
150 |
val remote_port: Int) |
|
151 |
{ |
|
152 |
override def toString: String = |
|
153 |
local_host + ":" + local_port + ":" + remote_host + ":" + remote_port |
|
154 |
||
155 |
def close() { ssh.session.delPortForwardingL(local_host, local_port) } |
|
65009 | 156 |
} |
157 |
||
158 |
||
64191 | 159 |
/* Sftp channel */ |
160 |
||
161 |
type Attrs = SftpATTRS |
|
162 |
||
64233 | 163 |
sealed case class Dir_Entry(name: Path, attrs: Attrs) |
64191 | 164 |
{ |
165 |
def is_file: Boolean = attrs.isReg |
|
166 |
def is_dir: Boolean = attrs.isDir |
|
167 |
} |
|
168 |
||
169 |
||
64132 | 170 |
/* exec channel */ |
171 |
||
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
172 |
private val exec_wait_delay = Time.seconds(0.3) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
173 |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
174 |
class Exec private[SSH](session: Session, channel: ChannelExec) |
64131 | 175 |
{ |
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
176 |
override def toString: String = "exec " + session.toString |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
177 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
178 |
def close() { channel.disconnect } |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
179 |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
180 |
val exit_status: Future[Int] = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
181 |
Future.thread("ssh_wait") { |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
182 |
while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
183 |
channel.getExitStatus |
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 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
186 |
val stdin: OutputStream = channel.getOutputStream |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
187 |
val stdout: InputStream = channel.getInputStream |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
188 |
val stderr: InputStream = channel.getErrStream |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
189 |
|
64166 | 190 |
// connect after preparing streams |
191 |
channel.connect(connect_timeout(session.options)) |
|
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
192 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
193 |
def result( |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
194 |
progress_stdout: String => Unit = (_: String) => (), |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
195 |
progress_stderr: String => Unit = (_: String) => (), |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
196 |
strict: Boolean = true): Process_Result = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
197 |
{ |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
198 |
stdin.close |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
199 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
200 |
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
|
201 |
{ |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
202 |
val result = new mutable.ListBuffer[String] |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
203 |
val line_buffer = new ByteArrayOutputStream(100) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
204 |
def line_flush() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
205 |
{ |
64326 | 206 |
val line = Library.trim_line(line_buffer.toString(UTF8.charset_name)) |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
207 |
progress(line) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
208 |
result += line |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
209 |
line_buffer.reset |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
210 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
211 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
212 |
var c = 0 |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
213 |
var finished = false |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
214 |
while (!finished) { |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
215 |
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
|
216 |
if (c == 10) line_flush() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
217 |
else if (channel.isClosed) { |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
218 |
if (line_buffer.size > 0) line_flush() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
219 |
finished = true |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
220 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
221 |
else Thread.sleep(exec_wait_delay.ms) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
222 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
223 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
224 |
result.toList |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
225 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
226 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
227 |
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
|
228 |
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
|
229 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
230 |
def terminate() |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
231 |
{ |
64136 | 232 |
close |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
233 |
out_lines.join |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
234 |
err_lines.join |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
235 |
exit_status.join |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
236 |
} |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
237 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
238 |
val rc = |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
239 |
try { exit_status.join } |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
240 |
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
241 |
|
64136 | 242 |
close |
64134
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
243 |
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
|
244 |
|
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
245 |
Process_Result(rc, out_lines.join, err_lines.join) |
57581e4026fe
proper support for exec channel (see also bash.scala);
wenzelm
parents:
64133
diff
changeset
|
246 |
} |
64131 | 247 |
} |
248 |
||
249 |
||
64123 | 250 |
/* session */ |
251 |
||
64166 | 252 |
class Session private[SSH](val options: Options, val session: JSch_Session) |
64123 | 253 |
{ |
64166 | 254 |
def update_options(new_options: Options): Session = new Session(new_options, session) |
255 |
||
64347 | 256 |
def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@" |
257 |
def host: String = if (session.getHost == null) "" else session.getHost |
|
258 |
def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort |
|
259 |
def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/" |
|
260 |
||
64123 | 261 |
override def toString: String = |
64347 | 262 |
user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)") |
64123 | 263 |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
264 |
|
65009 | 265 |
/* port forwarding */ |
266 |
||
65010 | 267 |
def port_forwarding(remote_port: Int, remote_host: String = "localhost", |
65009 | 268 |
local_port: Int = 0, local_host: String = "localhost"): Port_Forwarding = |
65010 | 269 |
Port_Forwarding.open(this, local_host, local_port, remote_host, remote_port) |
65009 | 270 |
|
271 |
||
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
272 |
/* sftp channel */ |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
273 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
274 |
val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp] |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
275 |
sftp.connect(connect_timeout(options)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
276 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
277 |
def close() { sftp.disconnect; session.disconnect } |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
278 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
279 |
val settings: Map[String, String] = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
280 |
{ |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
281 |
val home = sftp.getHome |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
282 |
Map("HOME" -> home, "USER_HOME" -> home) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
283 |
} |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
284 |
def expand_path(path: Path): Path = path.expand_env(settings) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
285 |
def remote_path(path: Path): String = expand_path(path).implode |
64304 | 286 |
def bash_path(path: Path): String = Bash.string(remote_path(path)) |
64123 | 287 |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
288 |
def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
289 |
def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
290 |
def rm(path: Path): Unit = sftp.rm(remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
291 |
def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
292 |
def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
293 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
294 |
def stat(path: Path): Option[Dir_Entry] = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
295 |
try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) } |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
296 |
catch { case _: SftpException => None } |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
297 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
298 |
def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
299 |
def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
300 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
301 |
def mkdirs(path: Path): Unit = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
302 |
if (!is_dir(path)) { |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
303 |
execute( |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
304 |
"perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"") |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
305 |
if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path))) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
306 |
} |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
307 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
308 |
def read_dir(path: Path): List[Dir_Entry] = |
64191 | 309 |
{ |
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
310 |
val dir = sftp.ls(remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
311 |
(for { |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
312 |
i <- (0 until dir.size).iterator |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
313 |
a = dir.get(i).asInstanceOf[AnyRef] |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
314 |
name = Untyped.get[String](a, "filename") |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
315 |
attrs = Untyped.get[Attrs](a, "attrs") |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
316 |
if name != "." && name != ".." |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
317 |
} yield Dir_Entry(Path.basic(name), attrs)).toList |
64191 | 318 |
} |
64135
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
wenzelm
parents:
64134
diff
changeset
|
319 |
|
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
320 |
def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
321 |
{ |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
322 |
def find(dir: Path): List[Dir_Entry] = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
323 |
read_dir(dir).flatMap(entry => |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
324 |
{ |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
325 |
val file = dir + entry.name |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
326 |
if (entry.is_dir) find(file) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
327 |
else if (pred(entry)) List(entry.copy(name = file)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
328 |
else Nil |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
329 |
}) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
330 |
find(root) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
331 |
} |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
332 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
333 |
def open_input(path: Path): InputStream = sftp.get(remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
334 |
def open_output(path: Path): OutputStream = sftp.put(remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
335 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
336 |
def read_file(path: Path, local_path: Path): Unit = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
337 |
sftp.get(remote_path(path), File.platform_path(local_path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
338 |
def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
339 |
def read(path: Path): String = using(open_input(path))(File.read_stream(_)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
340 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
341 |
def write_file(path: Path, local_path: Path): Unit = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
342 |
sftp.put(File.platform_path(local_path), remote_path(path)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
343 |
def write_bytes(path: Path, bytes: Bytes): Unit = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
344 |
using(open_output(path))(bytes.write_stream(_)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
345 |
def write(path: Path, text: String): Unit = |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
346 |
using(open_output(path))(stream => Bytes(text).write_stream(stream)) |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
347 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
348 |
|
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
349 |
/* exec channel */ |
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
350 |
|
64166 | 351 |
def exec(command: String): Exec = |
64129 | 352 |
{ |
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
353 |
val channel = session.openChannel("exec").asInstanceOf[ChannelExec] |
64190
c62b99e3ec07
provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
wenzelm
parents:
64185
diff
changeset
|
354 |
channel.setCommand("export USER_HOME=\"$HOME\"\n" + command) |
64256
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents:
64254
diff
changeset
|
355 |
new Exec(this, channel) |
64129 | 356 |
} |
64123 | 357 |
|
64191 | 358 |
def execute(command: String, |
359 |
progress_stdout: String => Unit = (_: String) => (), |
|
360 |
progress_stderr: String => Unit = (_: String) => (), |
|
361 |
strict: Boolean = true): Process_Result = |
|
362 |
exec(command).result(progress_stdout, progress_stderr, strict) |
|
64137 | 363 |
|
364 |
||
365 |
/* tmp dirs */ |
|
366 |
||
64306
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
wenzelm
parents:
64304
diff
changeset
|
367 |
def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) |
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
wenzelm
parents:
64304
diff
changeset
|
368 |
|
64137 | 369 |
def rm_tree(remote_dir: String): Unit = |
64304 | 370 |
execute("rm -r -f " + Bash.string(remote_dir)).check |
64137 | 371 |
|
372 |
def tmp_dir(): String = |
|
373 |
execute("mktemp -d -t tmp.XXXXXXXXXX").check.out |
|
374 |
||
64233 | 375 |
def with_tmp_dir[A](body: Path => A): A = |
64137 | 376 |
{ |
377 |
val remote_dir = tmp_dir() |
|
64233 | 378 |
try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } |
64137 | 379 |
} |
64123 | 380 |
} |
381 |
} |