26 def opt_template(s: String): String = optional(s, "--template") |
26 def opt_template(s: String): String = optional(s, "--template") |
27 |
27 |
28 |
28 |
29 /* repository access */ |
29 /* repository access */ |
30 |
30 |
31 def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean = |
31 def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = |
32 { |
32 ssh.is_dir(root + Path.explode(".hg")) && |
33 val root_hg = root + Path.explode(".hg") |
33 new Repository(root, ssh).command("root").ok |
34 val root_hg_present = |
|
35 ssh match { |
|
36 case None => root_hg.is_dir |
|
37 case Some(ssh) => ssh.is_dir(root_hg) |
|
38 } |
|
39 root_hg_present && new Repository(root, ssh).command("root").ok |
|
40 } |
|
41 |
34 |
42 def repository(root: Path, ssh: Option[SSH.Session] = None): Repository = |
35 def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = |
43 { |
36 { |
44 val hg = new Repository(root, ssh) |
37 val hg = new Repository(root, ssh) |
45 hg.command("root").check |
38 hg.command("root").check |
46 hg |
39 hg |
47 } |
40 } |
48 |
41 |
49 def find_repository(start: Path, ssh: Option[SSH.Session] = None): Option[Repository] = |
42 def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = |
50 { |
43 { |
51 def find(root: Path): Option[Repository] = |
44 def find(root: Path): Option[Repository] = |
52 if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) |
45 if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) |
53 else if (root.is_root) None |
46 else if (root.is_root) None |
54 else find(root + Path.parent) |
47 else find(root + Path.parent) |
55 |
48 |
56 ssh match { |
49 find(ssh.expand_path(start)) |
57 case None => find(start.expand) |
|
58 case Some(ssh) => find(ssh.expand_path(start)) |
|
59 } |
|
60 } |
50 } |
61 |
51 |
62 def clone_repository(source: String, root: Path, rev: String = "", options: String = "", |
52 def clone_repository(source: String, root: Path, rev: String = "", options: String = "", |
63 ssh: Option[SSH.Session] = None): Repository = |
53 ssh: SSH.System = SSH.Local): Repository = |
64 { |
54 { |
65 val hg = new Repository(root, ssh) |
55 val hg = new Repository(root, ssh) |
66 ssh match { |
56 ssh.mkdirs(hg.root.dir) |
67 case None => Isabelle_System.mkdirs(hg.root.dir) |
|
68 case Some(ssh) => ssh.mkdirs(hg.root.dir) |
|
69 } |
|
70 hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options) |
57 hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options) |
71 .check |
58 .check |
72 hg |
59 hg |
73 } |
60 } |
74 |
61 |
75 def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository = |
62 def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = |
76 { |
63 { |
77 val present = |
64 if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } |
78 ssh match { |
|
79 case None => root.is_dir |
|
80 case Some(ssh) => ssh.is_dir(root) |
|
81 } |
|
82 if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } |
|
83 else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
65 else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
84 } |
66 } |
85 |
67 |
86 class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session]) |
68 class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) |
87 { |
69 { |
88 hg => |
70 hg => |
89 |
71 |
90 val root = |
72 val root = ssh.expand_path(root_path) |
91 ssh match { |
73 def root_url: String = ssh.hg_url + root.implode |
92 case None => root_path.expand |
|
93 case Some(ssh) => ssh.expand_path(root_path) |
|
94 } |
|
95 |
74 |
96 def root_url: String = |
75 override def toString: String = ssh.prefix + root.implode |
97 ssh match { |
|
98 case None => root.implode |
|
99 case Some(ssh) => ssh.hg_url + root.implode |
|
100 } |
|
101 |
|
102 override def toString: String = |
|
103 ssh match { |
|
104 case None => root.implode |
|
105 case Some(ssh) => ssh.toString + ":" + root.implode |
|
106 } |
|
107 |
76 |
108 def command(name: String, args: String = "", options: String = ""): Process_Result = |
77 def command(name: String, args: String = "", options: String = ""): Process_Result = |
109 { |
78 { |
110 val cmdline = |
79 val cmdline = |
111 "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + |
80 "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + |
112 (if (name == "clone") "" else " --repository " + File.bash_path(root)) + |
81 (if (name == "clone") "" else " --repository " + File.bash_path(root)) + |
113 " --noninteractive " + name + " " + options + " " + args |
82 " --noninteractive " + name + " " + options + " " + args |
114 ssh match { |
83 ssh.execute(cmdline) |
115 case None => Isabelle_System.bash(cmdline) |
|
116 case Some(ssh) => ssh.execute(cmdline) |
|
117 } |
|
118 } |
84 } |
119 |
85 |
120 def archive(target: String, rev: String = "", options: String = ""): Unit = |
86 def archive(target: String, rev: String = "", options: String = ""): Unit = |
121 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check |
87 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check |
122 |
88 |