--- 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 */
--- 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]
--- 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
}