35 source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository = |
35 source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository = |
36 { |
36 { |
37 val hg = new Repository(root, ssh) |
37 val hg = new Repository(root, ssh) |
38 ssh match { |
38 ssh match { |
39 case None => Isabelle_System.mkdirs(hg.root.dir) |
39 case None => Isabelle_System.mkdirs(hg.root.dir) |
40 case Some(session) => using(session.sftp())(_.mkdirs(hg.root.dir)) |
40 case Some(ssh) => ssh.mkdirs(hg.root.dir) |
41 } |
41 } |
42 hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check |
42 hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check |
43 hg |
43 hg |
44 } |
44 } |
45 |
45 |
46 def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository = |
46 def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository = |
47 { |
47 { |
48 val present = |
48 val present = |
49 ssh match { |
49 ssh match { |
50 case None => root.is_dir |
50 case None => root.is_dir |
51 case Some(session) => using(session.sftp())(_.is_dir(root)) |
51 case Some(ssh) => ssh.is_dir(root) |
52 } |
52 } |
53 if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg } |
53 if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg } |
54 else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
54 else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
55 } |
55 } |
56 |
56 |
59 hg => |
59 hg => |
60 |
60 |
61 val root = |
61 val root = |
62 ssh match { |
62 ssh match { |
63 case None => root_path.expand |
63 case None => root_path.expand |
64 case Some(session) => using(session.sftp())(sftp => root_path.expand_env(sftp.settings)) |
64 case Some(ssh) => root_path.expand_env(ssh.settings) |
65 } |
65 } |
66 |
66 |
67 override def toString: String = |
67 override def toString: String = |
68 ssh match { |
68 ssh match { |
69 case None => root.implode |
69 case None => root.implode |
70 case Some(session) => session.toString + ":" + root.implode |
70 case Some(ssh) => ssh.toString + ":" + root.implode |
71 } |
71 } |
72 |
72 |
73 def command(name: String, args: String = "", options: String = ""): Process_Result = |
73 def command(name: String, args: String = "", options: String = ""): Process_Result = |
74 { |
74 { |
75 val cmdline = |
75 val cmdline = |
76 "\"${HG:-hg}\"" + |
76 "\"${HG:-hg}\"" + |
77 (if (name == "clone") "" else " --repository " + File.bash_path(root)) + |
77 (if (name == "clone") "" else " --repository " + File.bash_path(root)) + |
78 " --noninteractive " + name + " " + options + " " + args |
78 " --noninteractive " + name + " " + options + " " + args |
79 ssh match { |
79 ssh match { |
80 case None => Isabelle_System.bash(cmdline) |
80 case None => Isabelle_System.bash(cmdline) |
81 case Some(session) => session.execute(cmdline) |
81 case Some(ssh) => ssh.execute(cmdline) |
82 } |
82 } |
83 } |
83 } |
84 |
84 |
85 def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
85 def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
86 hg.command("heads", opt_template(template), options).check.out_lines |
86 hg.command("heads", opt_template(template), options).check.out_lines |