author | wenzelm |
Sat, 28 Nov 2020 15:15:53 +0100 | |
changeset 72755 | 8dffbe01a3e1 |
parent 72375 | e48d93811ed7 |
child 72763 | 3cc73d00553c |
permissions | -rw-r--r-- |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/mercurial.scala |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
3 |
|
64280 | 4 |
Support for Mercurial repositories, with local or remote repository clone |
5 |
and working directory (via ssh connection). |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
6 |
*/ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
7 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
9 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
10 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
11 |
import java.io.{File => JFile} |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
12 |
|
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
13 |
import scala.annotation.tailrec |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
14 |
import scala.collection.mutable |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
15 |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
16 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
17 |
object Mercurial |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
18 |
{ |
66895 | 19 |
type Graph = isabelle.Graph[String, Unit] |
20 |
||
21 |
||
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
22 |
/* command-line syntax */ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
23 |
|
63999 | 24 |
def optional(s: String, prefix: String = ""): String = |
64304 | 25 |
if (s == "") "" else " " + prefix + " " + Bash.string(s) |
63999 | 26 |
|
27 |
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else "" |
|
28 |
def opt_rev(s: String): String = optional(s, "--rev") |
|
29 |
def opt_template(s: String): String = optional(s, "--template") |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
30 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
31 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
32 |
/* repository access */ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
33 |
|
66570 | 34 |
def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = |
35 |
ssh.is_dir(root + Path.explode(".hg")) && |
|
36 |
new Repository(root, ssh).command("root").ok |
|
64330 | 37 |
|
66570 | 38 |
def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = |
64168 | 39 |
{ |
40 |
val hg = new Repository(root, ssh) |
|
41 |
hg.command("root").check |
|
42 |
hg |
|
43 |
} |
|
44 |
||
66570 | 45 |
def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = |
65559 | 46 |
{ |
71601 | 47 |
@tailrec def find(root: Path): Option[Repository] = |
65559 | 48 |
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) |
49 |
else if (root.is_root) None |
|
50 |
else find(root + Path.parent) |
|
51 |
||
66570 | 52 |
find(ssh.expand_path(start)) |
65559 | 53 |
} |
54 |
||
67066 | 55 |
private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local) |
56 |
: Repository = |
|
64168 | 57 |
{ |
64230 | 58 |
val hg = new Repository(root, ssh) |
72375 | 59 |
ssh.make_directory(hg.root.dir) |
67066 | 60 |
hg.command(cmd, args, repository = false).check |
64168 | 61 |
hg |
62 |
} |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
63 |
|
67065 | 64 |
def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository = |
67066 | 65 |
make_repository(root, "init", ssh.bash_path(root), ssh = ssh) |
67065 | 66 |
|
67 |
def clone_repository(source: String, root: Path, |
|
68 |
rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = |
|
69 |
make_repository(root, "clone", |
|
67066 | 70 |
options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) |
67065 | 71 |
|
66570 | 72 |
def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = |
64252
e84cba30d7ff
clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents:
64233
diff
changeset
|
73 |
{ |
66570 | 74 |
if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg } |
66105
8889aad1ff92
reverted 94cad7590015: does not help much on Windows;
wenzelm
parents:
66104
diff
changeset
|
75 |
else clone_repository(source, root, options = "--noupdate", ssh = ssh) |
64252
e84cba30d7ff
clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents:
64233
diff
changeset
|
76 |
} |
64230 | 77 |
|
66570 | 78 |
class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
79 |
{ |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
80 |
hg => |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
81 |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
82 |
val root: Path = ssh.expand_path(root_path) |
66570 | 83 |
def root_url: String = ssh.hg_url + root.implode |
64230 | 84 |
|
71562 | 85 |
override def toString: String = ssh.hg_url + root.implode |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
86 |
|
67065 | 87 |
def command(name: String, args: String = "", options: String = "", |
88 |
repository: Boolean = true): Process_Result = |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
89 |
{ |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
90 |
val cmdline = |
68566
38c8b44b40b9
more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
wenzelm
parents:
67782
diff
changeset
|
91 |
"export HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + |
67066 | 92 |
(if (repository) " --repository " + ssh.bash_path(root) else "") + |
64168 | 93 |
" --noninteractive " + name + " " + options + " " + args |
66570 | 94 |
ssh.execute(cmdline) |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
95 |
} |
63999 | 96 |
|
67068 | 97 |
def add(files: List[Path]): Unit = |
71601 | 98 |
hg.command("add", files.map(ssh.bash_path).mkString(" ")) |
67068 | 99 |
|
64505 | 100 |
def archive(target: String, rev: String = "", options: String = ""): Unit = |
101 |
hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check |
|
102 |
||
63999 | 103 |
def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
64168 | 104 |
hg.command("heads", opt_template(template), options).check.out_lines |
63999 | 105 |
|
64232
367d83d6030e
clarified hg.id operation, with explicit tip as default;
wenzelm
parents:
64230
diff
changeset
|
106 |
def identify(rev: String = "tip", options: String = ""): String = |
64168 | 107 |
hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" |
63998 | 108 |
|
64232
367d83d6030e
clarified hg.id operation, with explicit tip as default;
wenzelm
parents:
64230
diff
changeset
|
109 |
def id(rev: String = "tip"): String = identify(rev, options = "-i") |
367d83d6030e
clarified hg.id operation, with explicit tip as default;
wenzelm
parents:
64230
diff
changeset
|
110 |
|
71313 | 111 |
def paths(args: String = "", options: String = ""): List[String] = |
112 |
hg.command("paths", args = args, options = options).check.out_lines |
|
113 |
||
63998 | 114 |
def manifest(rev: String = "", options: String = ""): List[String] = |
64168 | 115 |
hg.command("manifest", opt_rev(rev), options).check.out_lines |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
116 |
|
64033 | 117 |
def log(rev: String = "", template: String = "", options: String = ""): String = |
64168 | 118 |
hg.command("log", opt_rev(rev) + opt_template(template), options).check.out |
64027 | 119 |
|
67755 | 120 |
def parent(): String = log(rev = "p1()", template = "{node|short}") |
121 |
||
64348
4c253e84ae62
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents:
64347
diff
changeset
|
122 |
def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "") |
4c253e84ae62
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents:
64347
diff
changeset
|
123 |
{ |
4c253e84ae62
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents:
64347
diff
changeset
|
124 |
hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options). |
64408
50bcf976f276
clarified hg push return code: 1 means "nothing to push";
wenzelm
parents:
64348
diff
changeset
|
125 |
check_rc(rc => rc == 0 | rc == 1) |
64348
4c253e84ae62
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents:
64347
diff
changeset
|
126 |
} |
4c253e84ae62
clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents:
64347
diff
changeset
|
127 |
|
63999 | 128 |
def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
64168 | 129 |
hg.command("pull", opt_rev(rev) + optional(remote), options).check |
63999 | 130 |
|
64168 | 131 |
def update( |
132 |
rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") |
|
63999 | 133 |
{ |
64168 | 134 |
hg.command("update", |
135 |
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check |
|
63999 | 136 |
} |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
137 |
|
65822
17b8528c2f53
clarified notion of known files (before actual commit);
wenzelm
parents:
65819
diff
changeset
|
138 |
def known_files(): List[String] = |
65825
11f87ab51ddb
more robust command invocation, without defaults from hgrc;
wenzelm
parents:
65822
diff
changeset
|
139 |
hg.command("status", options = "--modified --added --clean --no-status").check.out_lines |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
140 |
|
66895 | 141 |
def graph(): Graph = |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
142 |
{ |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
143 |
val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
144 |
val log_result = |
65825
11f87ab51ddb
more robust command invocation, without defaults from hgrc;
wenzelm
parents:
65822
diff
changeset
|
145 |
log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
146 |
(Graph.string[Unit] /: split_lines(log_result)) { |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
147 |
case (graph, Node(x, y, z)) => |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
148 |
val deps = List(y, z).filterNot(s => s.forall(_ == '0')) |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
149 |
val graph1 = (graph /: (x :: deps))(_.default_node(_, ())) |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
150 |
(graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) }) |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
151 |
case (graph, _) => graph |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
152 |
} |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
153 |
} |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
154 |
} |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
155 |
|
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
156 |
|
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
157 |
/* check files */ |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
158 |
|
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
159 |
def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
160 |
{ |
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
161 |
val outside = new mutable.ListBuffer[Path] |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
162 |
val unknown = new mutable.ListBuffer[Path] |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
163 |
|
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
164 |
@tailrec def check(paths: List[Path]) |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
165 |
{ |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
166 |
paths match { |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
167 |
case path :: rest => |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
168 |
find_repository(path, ssh) match { |
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
169 |
case None => outside += path; check(rest) |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
170 |
case Some(hg) => |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
171 |
val known = |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
172 |
hg.known_files().iterator.map(name => |
65833 | 173 |
(hg.root + Path.explode(name)).canonical_file).toSet |
174 |
if (!known(path.canonical_file)) unknown += path |
|
175 |
check(rest.filterNot(p => known(p.canonical_file))) |
|
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
176 |
} |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
177 |
case Nil => |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
178 |
} |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
179 |
} |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
180 |
|
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
181 |
check(files) |
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
182 |
(outside.toList, unknown.toList) |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
183 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
184 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
185 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
186 |
/* setup remote vs. local repository */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
187 |
|
71313 | 188 |
private def edit_hgrc(local_hg: Repository, path_name: String, source: String) |
189 |
{ |
|
190 |
val hgrc = local_hg.root + Path.explode(".hg/hgrc") |
|
191 |
def header(line: String): Boolean = line.startsWith("[paths]") |
|
192 |
val Entry = """^(\S+)\s*=\s*(.*)$""".r |
|
193 |
val new_entry = path_name + " = " + source |
|
194 |
||
195 |
def commit(lines: List[String]): Boolean = |
|
196 |
{ |
|
71320 | 197 |
File.write(hgrc, cat_lines(lines)) |
71313 | 198 |
true |
199 |
} |
|
200 |
val edited = |
|
201 |
hgrc.is_file && { |
|
202 |
val lines = split_lines(File.read(hgrc)) |
|
71383 | 203 |
lines.count(header) == 1 && { |
71313 | 204 |
if (local_hg.paths(options = "-q").contains(path_name)) { |
205 |
val old_source = local_hg.paths(args = path_name).head |
|
71320 | 206 |
val old_entry = path_name + ".old = " + old_source |
71313 | 207 |
val lines1 = |
208 |
lines.map { |
|
71320 | 209 |
case Entry(a, b) if a == path_name && b == old_source => |
210 |
new_entry + "\n" + old_entry |
|
71313 | 211 |
case line => line |
212 |
} |
|
213 |
lines != lines1 && commit(lines1) |
|
214 |
} |
|
215 |
else { |
|
216 |
val prefix = lines.takeWhile(line => !header(line)) |
|
217 |
val n = prefix.length |
|
218 |
commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1)) |
|
219 |
} |
|
220 |
} |
|
221 |
} |
|
222 |
if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n") |
|
223 |
} |
|
224 |
||
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
225 |
val default_path_name = "default" |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
226 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
227 |
def hg_setup( |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
228 |
remote: String, |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
229 |
local_path: Path, |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
230 |
remote_name: String = "", |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
231 |
path_name: String = default_path_name, |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
232 |
remote_exists: Boolean = false, |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71684
diff
changeset
|
233 |
progress: Progress = new Progress) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
234 |
{ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
235 |
/* local repository */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
236 |
|
72375 | 237 |
Isabelle_System.make_directory(local_path) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
238 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
239 |
val repos_name = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
240 |
proper_string(remote_name) getOrElse local_path.absolute.base.implode |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
241 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
242 |
val local_hg = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
243 |
if (is_repository(local_path)) repository(local_path) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
244 |
else init_repository(local_path) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
245 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
246 |
progress.echo("Local repository " + local_hg.root.absolute) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
247 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
248 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
249 |
/* remote repository */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
250 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
251 |
val remote_url = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
252 |
remote match { |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
253 |
case _ if remote.startsWith("ssh://") => |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
254 |
val ssh_url = remote + "/" + repos_name |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
255 |
|
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
256 |
if (!remote_exists) { |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
257 |
try { local_hg.command("init", ssh_url, repository = false).check } |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
258 |
catch { case ERROR(msg) => progress.echo_warning(msg) } |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
259 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
260 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
261 |
ssh_url |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
262 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
263 |
case SSH.Target(user, host) => |
71314 | 264 |
val phabricator = Phabricator.API(user, host) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
265 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
266 |
var repos = |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
267 |
phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
268 |
if (remote_exists) { |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
269 |
error("Remote repository " + |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
270 |
quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
271 |
} |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
272 |
else phabricator.create_repository(repos_name, short_name = repos_name) |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
273 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
274 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
275 |
while (repos.importing) { |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
276 |
progress.echo("Awaiting remote repository ...") |
71684 | 277 |
Time.seconds(0.5).sleep |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
278 |
repos = phabricator.the_repository(repos.phid) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
279 |
} |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
280 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
281 |
repos.ssh_url |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
282 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
283 |
case _ => error("Malformed remote specification " + quote(remote)) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
284 |
} |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
285 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
286 |
progress.echo("Remote repository " + quote(remote_url)) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
287 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
288 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
289 |
/* synchronize local and remote state */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
290 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
291 |
progress.echo("Synchronizing ...") |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
292 |
|
71313 | 293 |
edit_hgrc(local_hg, path_name, remote_url) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
294 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
295 |
local_hg.pull(options = "-u") |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
296 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
297 |
local_hg.push(remote = remote_url) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
298 |
} |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
299 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
300 |
val isabelle_tool = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
301 |
Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", args => |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
302 |
{ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
303 |
var remote_name = "" |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
304 |
var path_name = default_path_name |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
305 |
var remote_exists = false |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
306 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
307 |
val getopts = Getopts(""" |
71322 | 308 |
Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
309 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
310 |
Options are: |
71322 | 311 |
-n NAME remote repository name (default: base name of LOCAL_DIR) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
312 |
-p PATH Mercurial path name (default: """ + quote(default_path_name) + """) |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
313 |
-r assume that remote repository already exists |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
314 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
315 |
Setup a remote vs. local Mercurial repository: REMOTE either refers to a |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
316 |
Phabricator server "user@host" or SSH file server "ssh://user@host/path". |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
317 |
""", |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
318 |
"n:" -> (arg => remote_name = arg), |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
319 |
"p:" -> (arg => path_name = arg), |
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
320 |
"r" -> (_ => remote_exists = true)) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
321 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
322 |
val more_args = getopts(args) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
323 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
324 |
val (remote, local_path) = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
325 |
more_args match { |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
326 |
case List(arg1, arg2) => (arg1, Path.explode(arg2)) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
327 |
case _ => getopts.usage() |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
328 |
} |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
329 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
330 |
val progress = new Console_Progress |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
331 |
|
71319
26614beb3529
removed somewhat pointless option -R: more careful inspection of hgrc is required in practice;
wenzelm
parents:
71315
diff
changeset
|
332 |
hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name, |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
333 |
remote_exists = remote_exists, progress = progress) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
334 |
}) |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
335 |
} |