simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
--- a/src/Pure/Admin/build_history.scala Sun Oct 16 17:10:24 2016 +0200
+++ b/src/Pure/Admin/build_history.scala Sun Oct 16 17:44:37 2016 +0200
@@ -331,7 +331,7 @@
/** remote build_history -- via command-line **/
def remote_build_history(
- session: SSH.Session,
+ ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
isabelle_repos_source: String = "http://isabelle.in.tum.de/repos/isabelle",
@@ -340,37 +340,33 @@
options: String = "",
args: String = ""): List[(String, Bytes)] =
{
- using(session.sftp())(sftp =>
- {
- val isabelle_admin = sftp.remote_path(isabelle_repos_self + Path.explode("Admin"))
+ val isabelle_admin = ssh.remote_path(isabelle_repos_self + Path.explode("Admin"))
- /* prepare repository clones */
+ /* prepare repository clones */
- val isabelle_hg =
- Mercurial.setup_repository(
- isabelle_repos_source, isabelle_repos_self, ssh = Some(session))
+ val isabelle_hg =
+ Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
- if (self_update) {
- isabelle_hg.pull()
- isabelle_hg.update(clean = true)
- session.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
- }
+ if (self_update) {
+ isabelle_hg.pull()
+ isabelle_hg.update(clean = true)
+ ssh.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
+ }
- Mercurial.setup_repository(
- sftp.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(session))
+ Mercurial.setup_repository(
+ ssh.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
- /* Admin/build_history */
+ /* Admin/build_history */
- val result =
- session.execute(
- File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
- File.bash_string(sftp.remote_path(isabelle_repos_other)) + " " + args,
- progress_stderr = progress.echo(_)).check
+ val result =
+ ssh.execute(
+ File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
+ File.bash_string(ssh.remote_path(isabelle_repos_other)) + " " + args,
+ progress_stderr = progress.echo(_)).check
- for (line <- result.out_lines; log = Path.explode(line))
- yield (log.base.implode, sftp.read_bytes(log))
- })
+ for (line <- result.out_lines; log = Path.explode(line))
+ yield (log.base.implode, ssh.read_bytes(log))
}
}
--- a/src/Pure/Admin/remote_dmg.scala Sun Oct 16 17:10:24 2016 +0200
+++ b/src/Pure/Admin/remote_dmg.scala Sun Oct 16 17:44:37 2016 +0200
@@ -9,21 +9,20 @@
object Remote_DMG
{
- def remote_dmg(session: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
+ def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "")
{
- session.with_tmp_dir(remote_dir =>
- using(session.sftp())(sftp =>
- {
- val cd = "cd " + File.bash_string(sftp.remote_path(remote_dir)) + "; "
+ ssh.with_tmp_dir(remote_dir =>
+ {
+ val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; "
- sftp.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
- session.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
- session.execute(
- cd + "hdiutil create -srcfolder root" +
- (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
- " dmg.dmg").check
- sftp.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
- }))
+ ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
+ ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
+ ssh.execute(
+ cd + "hdiutil create -srcfolder root" +
+ (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
+ " dmg.dmg").check
+ ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
+ })
}
--- a/src/Pure/General/mercurial.scala Sun Oct 16 17:10:24 2016 +0200
+++ b/src/Pure/General/mercurial.scala Sun Oct 16 17:44:37 2016 +0200
@@ -37,7 +37,7 @@
val hg = new Repository(root, ssh)
ssh match {
case None => Isabelle_System.mkdirs(hg.root.dir)
- case Some(session) => using(session.sftp())(_.mkdirs(hg.root.dir))
+ case Some(ssh) => ssh.mkdirs(hg.root.dir)
}
hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
hg
@@ -48,7 +48,7 @@
val present =
ssh match {
case None => root.is_dir
- case Some(session) => using(session.sftp())(_.is_dir(root))
+ case Some(ssh) => ssh.is_dir(root)
}
if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
@@ -61,13 +61,13 @@
val root =
ssh match {
case None => root_path.expand
- case Some(session) => using(session.sftp())(sftp => root_path.expand_env(sftp.settings))
+ case Some(ssh) => root_path.expand_env(ssh.settings)
}
override def toString: String =
ssh match {
case None => root.implode
- case Some(session) => session.toString + ":" + root.implode
+ case Some(ssh) => ssh.toString + ":" + root.implode
}
def command(name: String, args: String = "", options: String = ""): Process_Result =
@@ -78,7 +78,7 @@
" --noninteractive " + name + " " + options + " " + args
ssh match {
case None => Isabelle_System.bash(cmdline)
- case Some(session) => session.execute(cmdline)
+ case Some(ssh) => ssh.execute(cmdline)
}
}
--- a/src/Pure/General/ssh.scala Sun Oct 16 17:10:24 2016 +0200
+++ b/src/Pure/General/ssh.scala Sun Oct 16 17:44:37 2016 +0200
@@ -103,17 +103,6 @@
}
- /* channel */
-
- class Channel[C <: JSch_Channel] private[SSH](
- val session: Session, val kind: String, val channel: C)
- {
- override def toString: String = kind + " " + session.toString
-
- def close() { channel.disconnect }
- }
-
-
/* Sftp channel */
type Attrs = SftpATTRS
@@ -124,88 +113,17 @@
def is_dir: Boolean = attrs.isDir
}
- class Sftp private[SSH](session: Session, kind: String, channel: ChannelSftp)
- extends Channel[ChannelSftp](session, kind, channel)
- {
- channel.connect(connect_timeout(session.options))
-
- val settings: Map[String, String] =
- {
- val home = channel.getHome
- Map("HOME" -> home, "USER_HOME" -> home)
- }
- def expand_path(path: Path): Path = path.expand_env(settings)
- def remote_path(path: Path): String = expand_path(path).implode
-
- def chmod(permissions: Int, path: Path): Unit = channel.chmod(permissions, remote_path(path))
- def mv(path1: Path, path2: Path): Unit = channel.rename(remote_path(path1), remote_path(path2))
- def rm(path: Path): Unit = channel.rm(remote_path(path))
- def mkdir(path: Path): Unit = channel.mkdir(remote_path(path))
- def rmdir(path: Path): Unit = channel.rmdir(remote_path(path))
-
- def stat(path: Path): Option[Dir_Entry] =
- try { Some(Dir_Entry(expand_path(path), channel.stat(remote_path(path)))) }
- catch { case _: SftpException => None }
-
- def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
- def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
-
- def mkdirs(path: Path): Unit =
- if (!is_dir(path)) {
- session.execute(
- "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
- if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
- }
-
- def read_dir(path: Path): List[Dir_Entry] =
- {
- val dir = channel.ls(remote_path(path))
- (for {
- i <- (0 until dir.size).iterator
- a = dir.get(i).asInstanceOf[AnyRef]
- name = Untyped.get[String](a, "filename")
- attrs = Untyped.get[Attrs](a, "attrs")
- if name != "." && name != ".."
- } yield Dir_Entry(Path.basic(name), attrs)).toList
- }
-
- def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
- {
- def find(dir: Path): List[Dir_Entry] =
- read_dir(dir).flatMap(entry =>
- {
- val file = dir + entry.name
- if (entry.is_dir) find(file)
- else if (pred(entry)) List(entry.copy(name = file))
- else Nil
- })
- find(root)
- }
-
- def open_input(path: Path): InputStream = channel.get(remote_path(path))
- def open_output(path: Path): OutputStream = channel.put(remote_path(path))
-
- def read_file(path: Path, local_path: Path): Unit =
- channel.get(remote_path(path), File.platform_path(local_path))
- def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
- def read(path: Path): String = using(open_input(path))(File.read_stream(_))
-
- def write_file(path: Path, local_path: Path): Unit =
- channel.put(File.platform_path(local_path), remote_path(path))
- def write_bytes(path: Path, bytes: Bytes): Unit =
- using(open_output(path))(bytes.write_stream(_))
- def write(path: Path, text: String): Unit =
- using(open_output(path))(stream => Bytes(text).write_stream(stream))
- }
-
/* exec channel */
private val exec_wait_delay = Time.seconds(0.3)
- class Exec private[SSH](session: Session, kind: String, channel: ChannelExec)
- extends Channel[ChannelExec](session, kind, channel)
+ class Exec private[SSH](session: Session, channel: ChannelExec)
{
+ override def toString: String = "exec " + session.toString
+
+ def close() { channel.disconnect }
+
def kill(signal: String) { channel.sendSignal(signal) }
val exit_status: Future[Int] =
@@ -290,21 +208,90 @@
(if (session.getPort == default_port) "" else ":" + session.getPort) +
(if (session.isConnected) "" else " (disconnected)")
- def close() { session.disconnect }
+
+ /* sftp channel */
+
+ val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
+ sftp.connect(connect_timeout(options))
+
+ def close() { sftp.disconnect; session.disconnect }
+
+ val settings: Map[String, String] =
+ {
+ val home = sftp.getHome
+ Map("HOME" -> home, "USER_HOME" -> home)
+ }
+ def expand_path(path: Path): Path = path.expand_env(settings)
+ def remote_path(path: Path): String = expand_path(path).implode
- def sftp(): Sftp =
+ def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
+ def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
+ def rm(path: Path): Unit = sftp.rm(remote_path(path))
+ def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path))
+ def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path))
+
+ def stat(path: Path): Option[Dir_Entry] =
+ try { Some(Dir_Entry(expand_path(path), sftp.stat(remote_path(path)))) }
+ catch { case _: SftpException => None }
+
+ def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
+ def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
+
+ def mkdirs(path: Path): Unit =
+ if (!is_dir(path)) {
+ execute(
+ "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
+ if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path)))
+ }
+
+ def read_dir(path: Path): List[Dir_Entry] =
{
- val kind = "sftp"
- val channel = session.openChannel(kind).asInstanceOf[ChannelSftp]
- new Sftp(this, kind, channel)
+ val dir = sftp.ls(remote_path(path))
+ (for {
+ i <- (0 until dir.size).iterator
+ a = dir.get(i).asInstanceOf[AnyRef]
+ name = Untyped.get[String](a, "filename")
+ attrs = Untyped.get[Attrs](a, "attrs")
+ if name != "." && name != ".."
+ } yield Dir_Entry(Path.basic(name), attrs)).toList
}
+ def find_files(root: Path, pred: Dir_Entry => Boolean = _ => true): List[Dir_Entry] =
+ {
+ def find(dir: Path): List[Dir_Entry] =
+ read_dir(dir).flatMap(entry =>
+ {
+ val file = dir + entry.name
+ if (entry.is_dir) find(file)
+ else if (pred(entry)) List(entry.copy(name = file))
+ else Nil
+ })
+ find(root)
+ }
+
+ def open_input(path: Path): InputStream = sftp.get(remote_path(path))
+ def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
+
+ def read_file(path: Path, local_path: Path): Unit =
+ sftp.get(remote_path(path), File.platform_path(local_path))
+ def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
+ def read(path: Path): String = using(open_input(path))(File.read_stream(_))
+
+ def write_file(path: Path, local_path: Path): Unit =
+ sftp.put(File.platform_path(local_path), remote_path(path))
+ def write_bytes(path: Path, bytes: Bytes): Unit =
+ using(open_output(path))(bytes.write_stream(_))
+ def write(path: Path, text: String): Unit =
+ using(open_output(path))(stream => Bytes(text).write_stream(stream))
+
+
+ /* exec channel */
+
def exec(command: String): Exec =
{
- val kind = "exec"
- val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
+ val channel = session.openChannel("exec").asInstanceOf[ChannelExec]
channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
- new Exec(this, kind, channel)
+ new Exec(this, channel)
}
def execute(command: String,