| author | paulson <lp15@cam.ac.uk> | 
| Sat, 05 Aug 2017 16:18:35 +0200 | |
| changeset 66342 | d8c7ca0e01c6 | 
| parent 65717 | 556c34fd0554 | 
| child 66570 | 9af879e222cc | 
| 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 =  | 
| 65717 | 80  | 
jsch.getSession(proper_string(user) getOrElse null, host,  | 
81  | 
if (port > 0) port else default_port)  | 
|
| 64257 | 82  | 
|
83  | 
session.setUserInfo(No_User_Info)  | 
|
| 64325 | 84  | 
session.setServerAliveInterval(alive_interval(options))  | 
| 64257 | 85  | 
      session.setConfig("MaxAuthTries", "3")
 | 
86  | 
||
87  | 
      if (options.bool("ssh_compression")) {
 | 
|
88  | 
        session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
 | 
|
89  | 
        session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none")
 | 
|
90  | 
        session.setConfig("compression_level", "9")
 | 
|
91  | 
}  | 
|
92  | 
||
93  | 
session.connect(connect_timeout(options))  | 
|
94  | 
new Session(options, session)  | 
|
95  | 
}  | 
|
96  | 
}  | 
|
| 64130 | 97  | 
|
| 64123 | 98  | 
|
99  | 
/* logging */  | 
|
100  | 
||
101  | 
def logging(verbose: Boolean = true, debug: Boolean = false)  | 
|
102  | 
  {
 | 
|
103  | 
JSch.setLogger(if (verbose) new Logger(debug) else null)  | 
|
104  | 
}  | 
|
105  | 
||
106  | 
private class Logger(debug: Boolean) extends JSch_Logger  | 
|
107  | 
  {
 | 
|
108  | 
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug  | 
|
109  | 
||
110  | 
def log(level: Int, msg: String)  | 
|
111  | 
    {
 | 
|
112  | 
      level match {
 | 
|
113  | 
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)  | 
|
114  | 
case JSch_Logger.WARN => Output.warning(msg)  | 
|
115  | 
case _ => Output.writeln(msg)  | 
|
116  | 
}  | 
|
117  | 
}  | 
|
118  | 
}  | 
|
119  | 
||
120  | 
||
| 64128 | 121  | 
/* user info */  | 
122  | 
||
123  | 
object No_User_Info extends UserInfo  | 
|
124  | 
  {
 | 
|
125  | 
def getPassphrase: String = null  | 
|
126  | 
def getPassword: String = null  | 
|
127  | 
def promptPassword(msg: String): Boolean = false  | 
|
128  | 
def promptPassphrase(msg: String): Boolean = false  | 
|
129  | 
def promptYesNo(msg: String): Boolean = false  | 
|
130  | 
def showMessage(msg: String): Unit = Output.writeln(msg)  | 
|
131  | 
}  | 
|
132  | 
||
133  | 
||
| 65009 | 134  | 
/* port forwarding */  | 
135  | 
||
| 65010 | 136  | 
object Port_Forwarding  | 
| 65009 | 137  | 
  {
 | 
| 
65636
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
138  | 
def open(ssh: Session, ssh_close: Boolean,  | 
| 65010 | 139  | 
local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding =  | 
140  | 
    {
 | 
|
141  | 
val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port)  | 
|
| 
65636
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
142  | 
new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port)  | 
| 65010 | 143  | 
}  | 
144  | 
}  | 
|
145  | 
||
146  | 
class Port_Forwarding private[SSH](  | 
|
147  | 
ssh: SSH.Session,  | 
|
| 
65636
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
148  | 
ssh_close: Boolean,  | 
| 65010 | 149  | 
val local_host: String,  | 
150  | 
val local_port: Int,  | 
|
151  | 
val remote_host: String,  | 
|
152  | 
val remote_port: Int)  | 
|
153  | 
  {
 | 
|
154  | 
override def toString: String =  | 
|
155  | 
local_host + ":" + local_port + ":" + remote_host + ":" + remote_port  | 
|
156  | 
||
| 
65636
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
157  | 
def close()  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
158  | 
    {
 | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
159  | 
ssh.session.delPortForwardingL(local_host, local_port)  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
160  | 
if (ssh_close) ssh.close()  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
161  | 
}  | 
| 65009 | 162  | 
}  | 
163  | 
||
164  | 
||
| 64191 | 165  | 
/* Sftp channel */  | 
166  | 
||
167  | 
type Attrs = SftpATTRS  | 
|
168  | 
||
| 64233 | 169  | 
sealed case class Dir_Entry(name: Path, attrs: Attrs)  | 
| 64191 | 170  | 
  {
 | 
171  | 
def is_file: Boolean = attrs.isReg  | 
|
172  | 
def is_dir: Boolean = attrs.isDir  | 
|
173  | 
}  | 
|
174  | 
||
175  | 
||
| 64132 | 176  | 
/* exec channel */  | 
177  | 
||
| 
64134
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
178  | 
private val exec_wait_delay = Time.seconds(0.3)  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
179  | 
|
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
180  | 
class Exec private[SSH](session: Session, channel: ChannelExec)  | 
| 64131 | 181  | 
  {
 | 
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
182  | 
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
 | 
183  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
184  | 
    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
 | 
185  | 
|
| 
64134
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
186  | 
val exit_status: Future[Int] =  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
187  | 
      Future.thread("ssh_wait") {
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
188  | 
while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms)  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
189  | 
channel.getExitStatus  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
190  | 
}  | 
| 
 
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  | 
val stdin: OutputStream = channel.getOutputStream  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
193  | 
val stdout: InputStream = channel.getInputStream  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
194  | 
val stderr: InputStream = channel.getErrStream  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
195  | 
|
| 64166 | 196  | 
// connect after preparing streams  | 
197  | 
channel.connect(connect_timeout(session.options))  | 
|
| 
64134
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
198  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
199  | 
def result(  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
200  | 
progress_stdout: String => Unit = (_: String) => (),  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
201  | 
progress_stderr: String => Unit = (_: String) => (),  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
202  | 
strict: Boolean = true): Process_Result =  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
203  | 
    {
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
204  | 
stdin.close  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
205  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
206  | 
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
 | 
207  | 
      {
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
208  | 
val result = new mutable.ListBuffer[String]  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
209  | 
val line_buffer = new ByteArrayOutputStream(100)  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
210  | 
def line_flush()  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
211  | 
        {
 | 
| 64326 | 212  | 
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
 | 
213  | 
progress(line)  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
214  | 
result += line  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
215  | 
line_buffer.reset  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
216  | 
}  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
217  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
218  | 
var c = 0  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
219  | 
var finished = false  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
220  | 
        while (!finished) {
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
221  | 
          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
 | 
222  | 
if (c == 10) line_flush()  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
223  | 
          else if (channel.isClosed) {
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
224  | 
if (line_buffer.size > 0) line_flush()  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
225  | 
finished = true  | 
| 
 
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  | 
else Thread.sleep(exec_wait_delay.ms)  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
228  | 
}  | 
| 
 
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  | 
result.toList  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
231  | 
}  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
232  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
233  | 
      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
 | 
234  | 
      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
 | 
235  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
236  | 
def terminate()  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
237  | 
      {
 | 
| 64136 | 238  | 
close  | 
| 
64134
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
239  | 
out_lines.join  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
240  | 
err_lines.join  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
241  | 
exit_status.join  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
242  | 
}  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
243  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
244  | 
val rc =  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
245  | 
        try { exit_status.join }
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
246  | 
        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
247  | 
|
| 64136 | 248  | 
close  | 
| 
64134
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
249  | 
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
 | 
250  | 
|
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
251  | 
Process_Result(rc, out_lines.join, err_lines.join)  | 
| 
 
57581e4026fe
proper support for exec channel (see also bash.scala);
 
wenzelm 
parents: 
64133 
diff
changeset
 | 
252  | 
}  | 
| 64131 | 253  | 
}  | 
254  | 
||
255  | 
||
| 64123 | 256  | 
/* session */  | 
257  | 
||
| 64166 | 258  | 
class Session private[SSH](val options: Options, val session: JSch_Session)  | 
| 64123 | 259  | 
  {
 | 
| 64166 | 260  | 
def update_options(new_options: Options): Session = new Session(new_options, session)  | 
261  | 
||
| 64347 | 262  | 
def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"  | 
263  | 
def host: String = if (session.getHost == null) "" else session.getHost  | 
|
264  | 
def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort  | 
|
265  | 
def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"  | 
|
266  | 
||
| 64123 | 267  | 
override def toString: String =  | 
| 64347 | 268  | 
user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")  | 
| 64123 | 269  | 
|
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
270  | 
|
| 65009 | 271  | 
/* port forwarding */  | 
272  | 
||
| 
65636
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
273  | 
def port_forwarding(  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
274  | 
remote_port: Int, remote_host: String = "localhost",  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
275  | 
local_port: Int = 0, local_host: String = "localhost",  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
276  | 
ssh_close: Boolean = false): Port_Forwarding =  | 
| 
 
df804cdba5f9
ssh_close for proper termination after use of database;
 
wenzelm 
parents: 
65594 
diff
changeset
 | 
277  | 
Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port)  | 
| 65009 | 278  | 
|
279  | 
||
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
280  | 
/* sftp channel */  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
281  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
282  | 
    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
 | 
283  | 
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
 | 
284  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
285  | 
    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
 | 
286  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
287  | 
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
 | 
288  | 
    {
 | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
289  | 
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
 | 
290  | 
      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
 | 
291  | 
}  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
292  | 
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
 | 
293  | 
def remote_path(path: Path): String = expand_path(path).implode  | 
| 64304 | 294  | 
def bash_path(path: Path): String = Bash.string(remote_path(path))  | 
| 64123 | 295  | 
|
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
296  | 
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
 | 
297  | 
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
 | 
298  | 
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
 | 
299  | 
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
 | 
300  | 
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
 | 
301  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
302  | 
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
 | 
303  | 
      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
 | 
304  | 
      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
 | 
305  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
306  | 
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
 | 
307  | 
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
 | 
308  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
309  | 
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
 | 
310  | 
      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
 | 
311  | 
execute(  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
312  | 
          "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
 | 
313  | 
        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
 | 
314  | 
}  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
315  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
316  | 
def read_dir(path: Path): List[Dir_Entry] =  | 
| 64191 | 317  | 
    {
 | 
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
318  | 
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
 | 
319  | 
      (for {
 | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
320  | 
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
 | 
321  | 
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
 | 
322  | 
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
 | 
323  | 
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
 | 
324  | 
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
 | 
325  | 
} yield Dir_Entry(Path.basic(name), attrs)).toList  | 
| 64191 | 326  | 
}  | 
| 
64135
 
865dda40e1cc
provide execute operation, similar to Isabelle_System.bash;
 
wenzelm 
parents: 
64134 
diff
changeset
 | 
327  | 
|
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
328  | 
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
 | 
329  | 
    {
 | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
330  | 
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
 | 
331  | 
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
 | 
332  | 
          {
 | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
333  | 
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
 | 
334  | 
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
 | 
335  | 
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
 | 
336  | 
else Nil  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
337  | 
})  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
338  | 
find(root)  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
339  | 
}  | 
| 
 
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 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
 | 
342  | 
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
 | 
343  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
344  | 
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
 | 
345  | 
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
 | 
346  | 
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
 | 
347  | 
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
 | 
348  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
349  | 
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
 | 
350  | 
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
 | 
351  | 
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
 | 
352  | 
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
 | 
353  | 
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
 | 
354  | 
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
 | 
355  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
356  | 
|
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
357  | 
/* exec channel */  | 
| 
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
358  | 
|
| 64166 | 359  | 
def exec(command: String): Exec =  | 
| 64129 | 360  | 
    {
 | 
| 
64256
 
c3197aeae90b
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
 
wenzelm 
parents: 
64254 
diff
changeset
 | 
361  | 
      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
 | 
362  | 
      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
 | 
363  | 
new Exec(this, channel)  | 
| 64129 | 364  | 
}  | 
| 64123 | 365  | 
|
| 64191 | 366  | 
def execute(command: String,  | 
367  | 
progress_stdout: String => Unit = (_: String) => (),  | 
|
368  | 
progress_stderr: String => Unit = (_: String) => (),  | 
|
369  | 
strict: Boolean = true): Process_Result =  | 
|
370  | 
exec(command).result(progress_stdout, progress_stderr, strict)  | 
|
| 64137 | 371  | 
|
372  | 
||
373  | 
/* tmp dirs */  | 
|
374  | 
||
| 
64306
 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 
wenzelm 
parents: 
64304 
diff
changeset
 | 
375  | 
def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir))  | 
| 
 
7b6dc1b36f20
tuned signature, in accordance to Isabelle_System;
 
wenzelm 
parents: 
64304 
diff
changeset
 | 
376  | 
|
| 64137 | 377  | 
def rm_tree(remote_dir: String): Unit =  | 
| 64304 | 378  | 
      execute("rm -r -f " + Bash.string(remote_dir)).check
 | 
| 64137 | 379  | 
|
380  | 
def tmp_dir(): String =  | 
|
381  | 
      execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
 | 
|
382  | 
||
| 64233 | 383  | 
def with_tmp_dir[A](body: Path => A): A =  | 
| 64137 | 384  | 
    {
 | 
385  | 
val remote_dir = tmp_dir()  | 
|
| 64233 | 386  | 
      try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
 | 
| 64137 | 387  | 
}  | 
| 64123 | 388  | 
}  | 
389  | 
}  |