# HG changeset patch
# User wenzelm
# Date 1476632677 -7200
# Node ID c3197aeae90b31da07b9b26edd6dade4d2adc37c
# Parent  a9f5408816118aef5fa2353672f7cb04cc9fe6aa
simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;

diff -r a9f540881611 -r c3197aeae90b src/Pure/Admin/build_history.scala
--- 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))
   }
 }
diff -r a9f540881611 -r c3197aeae90b src/Pure/Admin/remote_dmg.scala
--- 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)
+      })
   }
 
 
diff -r a9f540881611 -r c3197aeae90b src/Pure/General/mercurial.scala
--- 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)
       }
     }
 
diff -r a9f540881611 -r c3197aeae90b src/Pure/General/ssh.scala
--- 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,