# HG changeset patch
# User wenzelm
# Date 1504172530 -7200
# Node ID 9af879e222ccfeff49ea3d1deea00ec66e8109c7
# Parent  1a475e59c70fcc4bd5d55081141393ad149746b8
clarified signature;
tuned ssh.prefix;

diff -r 1a475e59c70f -r 9af879e222cc src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Thu Aug 31 11:15:38 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Aug 31 11:42:10 2017 +0200
@@ -439,7 +439,7 @@
     /* prepare repository clones */
 
     val isabelle_hg =
-      Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = Some(ssh))
+      Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
 
     if (self_update) {
       val self_rev =
@@ -460,12 +460,12 @@
       ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
     }
 
-    if (Mercurial.is_repository(isabelle_repos_other, ssh = Some(ssh))) {
+    if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
       ssh.rm_tree(isabelle_repos_other)
     }
     val other_hg =
       Mercurial.clone_repository(
-        ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = Some(ssh))
+        ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = ssh)
 
 
     /* Admin/build_history */
diff -r 1a475e59c70f -r 9af879e222cc src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Thu Aug 31 11:15:38 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Thu Aug 31 11:42:10 2017 +0200
@@ -28,82 +28,51 @@
 
   /* repository access */
 
-  def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
-  {
-    val root_hg = root + Path.explode(".hg")
-    val root_hg_present =
-      ssh match {
-        case None => root_hg.is_dir
-        case Some(ssh) => ssh.is_dir(root_hg)
-      }
-    root_hg_present && new Repository(root, ssh).command("root").ok
-  }
+  def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
+    ssh.is_dir(root + Path.explode(".hg")) &&
+    new Repository(root, ssh).command("root").ok
 
-  def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
+  def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
   {
     val hg = new Repository(root, ssh)
     hg.command("root").check
     hg
   }
 
-  def find_repository(start: Path, ssh: Option[SSH.Session] = None): Option[Repository] =
+  def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
   {
     def find(root: Path): Option[Repository] =
       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
       else if (root.is_root) None
       else find(root + Path.parent)
 
-    ssh match {
-      case None => find(start.expand)
-      case Some(ssh) => find(ssh.expand_path(start))
-    }
+    find(ssh.expand_path(start))
   }
 
   def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
-    ssh: Option[SSH.Session] = None): Repository =
+    ssh: SSH.System = SSH.Local): Repository =
   {
     val hg = new Repository(root, ssh)
-    ssh match {
-      case None => Isabelle_System.mkdirs(hg.root.dir)
-      case Some(ssh) => ssh.mkdirs(hg.root.dir)
-    }
+    ssh.mkdirs(hg.root.dir)
     hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
       .check
     hg
   }
 
-  def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =
+  def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
   {
-    val present =
-      ssh match {
-        case None => root.is_dir
-        case Some(ssh) => ssh.is_dir(root)
-      }
-    if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
+    if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   }
 
-  class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
+  class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
   {
     hg =>
 
-    val root =
-      ssh match {
-        case None => root_path.expand
-        case Some(ssh) => ssh.expand_path(root_path)
-      }
+    val root = ssh.expand_path(root_path)
+    def root_url: String = ssh.hg_url + root.implode
 
-    def root_url: String =
-      ssh match {
-        case None => root.implode
-        case Some(ssh) => ssh.hg_url + root.implode
-      }
-
-    override def toString: String =
-      ssh match {
-        case None => root.implode
-        case Some(ssh) => ssh.toString + ":" + root.implode
-      }
+    override def toString: String = ssh.prefix + root.implode
 
     def command(name: String, args: String = "", options: String = ""): Process_Result =
     {
@@ -111,10 +80,7 @@
         "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
           (if (name == "clone") "" else " --repository " + File.bash_path(root)) +
           " --noninteractive " + name + " " + options + " " + args
-      ssh match {
-        case None => Isabelle_System.bash(cmdline)
-        case Some(ssh) => ssh.execute(cmdline)
-      }
+      ssh.execute(cmdline)
     }
 
     def archive(target: String, rev: String = "", options: String = ""): Unit =
@@ -171,7 +137,7 @@
 
   /* unknown files */
 
-  def unknown_files(files: List[Path], ssh: Option[SSH.Session] = None): List[Path] =
+  def unknown_files(files: List[Path], ssh: SSH.System = SSH.Local): List[Path] =
   {
     val unknown = new mutable.ListBuffer[Path]
 
diff -r 1a475e59c70f -r 9af879e222cc src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Aug 31 11:15:38 2017 +0200
+++ b/src/Pure/General/ssh.scala	Thu Aug 31 11:42:10 2017 +0200
@@ -255,14 +255,17 @@
 
   /* session */
 
-  class Session private[SSH](val options: Options, val session: JSch_Session)
+  class Session private[SSH](val options: Options, val session: JSch_Session) extends System
   {
     def update_options(new_options: Options): Session = new Session(new_options, session)
 
     def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
     def host: String = if (session.getHost == null) "" else session.getHost
     def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
-    def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+    override def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+
+    override def prefix: String =
+      user_prefix + host + port_suffix + ":"
 
     override def toString: String =
       user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
@@ -289,7 +292,7 @@
       val home = sftp.getHome
       Map("HOME" -> home, "USER_HOME" -> home)
     }
-    def expand_path(path: Path): Path = path.expand_env(settings)
+    override def expand_path(path: Path): Path = path.expand_env(settings)
     def remote_path(path: Path): String = expand_path(path).implode
     def bash_path(path: Path): String = Bash.string(remote_path(path))
 
@@ -303,10 +306,10 @@
       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
+    override def is_file(path: Path): Boolean = stat(path).map(_.is_file) getOrElse false
+    override def is_dir(path: Path): Boolean = stat(path).map(_.is_dir) getOrElse false
 
-    def mkdirs(path: Path): Unit =
+    override def mkdirs(path: Path): Unit =
       if (!is_dir(path)) {
         execute(
           "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"")
@@ -363,7 +366,7 @@
       new Exec(this, channel)
     }
 
-    def execute(command: String,
+    override def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
         strict: Boolean = true): Process_Result =
@@ -386,4 +389,28 @@
       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
     }
   }
+
+
+
+  /* system operations */
+
+  trait System
+  {
+    def hg_url: String = ""
+    def prefix: String = ""
+
+    def expand_path(path: Path): Path = path.expand
+    def is_file(path: Path): Boolean = path.is_file
+    def is_dir(path: Path): Boolean = path.is_dir
+    def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)
+
+    def execute(command: String,
+        progress_stdout: String => Unit = (_: String) => (),
+        progress_stderr: String => Unit = (_: String) => (),
+        strict: Boolean = true): Process_Result =
+      Isabelle_System.bash(command, progress_stdout = progress_stdout,
+        progress_stderr = progress_stderr, strict = strict)
+  }
+
+  object Local extends System
 }