author | wenzelm |
Mon, 13 Mar 2023 11:02:26 +0100 | |
changeset 77622 | f458547b4f0f |
parent 77518 | fda4da0f80f4 |
child 77782 | 127d077cccfe |
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 |
|
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
11 |
import scala.annotation.tailrec |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
12 |
import scala.collection.mutable |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
13 |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
14 |
|
75393 | 15 |
object Mercurial { |
66895 | 16 |
type Graph = isabelle.Graph[String, Unit] |
17 |
||
18 |
||
75472 | 19 |
|
20 |
/** HTTP server **/ |
|
73611 | 21 |
|
75393 | 22 |
object Server { |
73611 | 23 |
def apply(root: String): Server = new Server(root) |
24 |
||
75393 | 25 |
def start(root: Path): Server = { |
73611 | 26 |
val hg = repository(root) |
73609 | 27 |
|
73611 | 28 |
val server_process = Future.promise[Bash.Process] |
29 |
val server_root = Future.promise[String] |
|
30 |
Isabelle_Thread.fork("hg") { |
|
31 |
val process = |
|
32 |
Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) } |
|
33 |
server_process.fulfill_result(process) |
|
34 |
Exn.release(process).result(progress_stdout = |
|
35 |
line => if (!server_root.is_finished) { |
|
36 |
server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line)) |
|
37 |
}) |
|
38 |
} |
|
39 |
server_process.join |
|
40 |
||
41 |
new Server(server_root.join) { |
|
42 |
override def close(): Unit = server_process.join.terminate() |
|
43 |
} |
|
44 |
} |
|
73609 | 45 |
} |
46 |
||
75393 | 47 |
class Server private(val root: String) extends AutoCloseable { |
73609 | 48 |
override def toString: String = root |
49 |
||
73611 | 50 |
def close(): Unit = () |
51 |
||
73610 | 52 |
def changeset(rev: String = "tip", raw: Boolean = false): String = |
53 |
root + (if (raw) "/raw-rev/" else "/rev/") + rev |
|
54 |
||
55 |
def file(path: Path, rev: String = "tip", raw: Boolean = false): String = |
|
76883 | 56 |
root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + File.standard_path(path) |
73610 | 57 |
|
58 |
def archive(rev: String = "tip"): String = |
|
59 |
root + "/archive/" + rev + ".tar.gz" |
|
60 |
||
61 |
def read_changeset(rev: String = "tip"): String = |
|
62 |
Url.read(changeset(rev = rev, raw = true)) |
|
63 |
||
64 |
def read_file(path: Path, rev: String = "tip"): String = |
|
65 |
Url.read(file(path, rev = rev, raw = true)) |
|
66 |
||
67 |
def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content = |
|
68 |
Isabelle_System.download(archive(rev = rev), progress = progress) |
|
69 |
||
75393 | 70 |
def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = { |
73610 | 71 |
Isabelle_System.new_directory(dir) |
75394 | 72 |
Isabelle_System.with_tmp_file("rev", ext = ".tar.gz") { archive_path => |
73610 | 73 |
val content = download_archive(rev = rev, progress = progress) |
74 |
Bytes.write(archive_path, content.bytes) |
|
75 |
progress.echo("Unpacking " + rev + ".tar.gz") |
|
73624 | 76 |
Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path), |
76540
83de6e9ae983
clarified signature: prefer Scala functions instead of shell scripts;
wenzelm
parents:
76169
diff
changeset
|
77 |
dir = dir, original_owner = true, strip = true).check |
75394 | 78 |
} |
73610 | 79 |
} |
73609 | 80 |
} |
81 |
||
82 |
||
75472 | 83 |
|
84 |
/** repository commands **/ |
|
85 |
||
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
86 |
/* command-line syntax */ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
87 |
|
63999 | 88 |
def optional(s: String, prefix: String = ""): String = |
77368 | 89 |
if_proper(s, " " + prefix + " " + Bash.string(s)) |
63999 | 90 |
|
91 |
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else "" |
|
92 |
def opt_rev(s: String): String = optional(s, "--rev") |
|
93 |
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
|
94 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
95 |
|
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
96 |
/* repository archives */ |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
97 |
|
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
98 |
private val Archive_Node = """^node: (\S{12}).*$""".r |
73521 | 99 |
private val Archive_Tag = """^tag: (\S+).*$""".r |
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
100 |
|
75393 | 101 |
sealed case class Archive_Info(lines: List[String]) { |
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
102 |
def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a }) |
73521 | 103 |
def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag |
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
104 |
} |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
105 |
|
75393 | 106 |
def archive_info(root: Path): Option[Archive_Info] = { |
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
107 |
val path = root + Path.explode(".hg_archival.txt") |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
108 |
if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
109 |
} |
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
110 |
|
73521 | 111 |
def archive_id(root: Path): Option[String] = |
112 |
archive_info(root).flatMap(_.id) |
|
113 |
||
114 |
def archive_tags(root: Path): Option[String] = |
|
115 |
archive_info(root).map(info => info.tags.mkString(" ")) |
|
73520
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
116 |
|
4cba4e250c28
clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents:
73483
diff
changeset
|
117 |
|
75511 | 118 |
/* hg_sync meta data */ |
119 |
||
75514 | 120 |
object Hg_Sync { |
121 |
val NAME = ".hg_sync" |
|
122 |
val _NAME: String = " " + NAME |
|
123 |
val PATH: Path = Path.explode(NAME) |
|
124 |
val PATH_ID: Path = PATH + Path.explode("id") |
|
125 |
val PATH_LOG: Path = PATH + Path.explode("log") |
|
126 |
val PATH_DIFF: Path = PATH + Path.explode("diff") |
|
127 |
val PATH_STAT: Path = PATH + Path.explode("stat") |
|
128 |
||
129 |
def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = |
|
130 |
ssh.is_dir(root + PATH) |
|
131 |
||
132 |
def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = { |
|
133 |
if (is_directory(root, ssh = ssh)) new Directory(root, ssh) |
|
134 |
else error("No .hg_sync directory found in " + ssh.rsync_path(root)) |
|
135 |
} |
|
136 |
||
137 |
class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System) |
|
138 |
{ |
|
139 |
override def toString: String = ssh.rsync_path(root) |
|
140 |
||
141 |
def read(path: Path): String = ssh.read(root + path) |
|
142 |
lazy val id: String = read(PATH_ID) |
|
143 |
lazy val log: String = read(PATH_LOG) |
|
144 |
lazy val diff: String = read(PATH_DIFF) |
|
145 |
lazy val stat: String = read(PATH_STAT) |
|
146 |
||
147 |
def changed: Boolean = id.endsWith("+") |
|
148 |
} |
|
149 |
} |
|
75511 | 150 |
|
151 |
||
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
152 |
/* repository access */ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
153 |
|
66570 | 154 |
def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = |
155 |
ssh.is_dir(root + Path.explode(".hg")) && |
|
156 |
new Repository(root, ssh).command("root").ok |
|
64330 | 157 |
|
75510 | 158 |
def id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] = |
159 |
if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None |
|
160 |
||
75393 | 161 |
def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = { |
64168 | 162 |
val hg = new Repository(root, ssh) |
163 |
hg.command("root").check |
|
164 |
hg |
|
165 |
} |
|
166 |
||
75506 | 167 |
def self_repository(): Repository = repository(Path.ISABELLE_HOME) |
168 |
||
75393 | 169 |
def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = { |
71601 | 170 |
@tailrec def find(root: Path): Option[Repository] = |
65559 | 171 |
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) |
172 |
else if (root.is_root) None |
|
173 |
else find(root + Path.parent) |
|
174 |
||
66570 | 175 |
find(ssh.expand_path(start)) |
65559 | 176 |
} |
177 |
||
75474 | 178 |
def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository = |
179 |
find_repository(start, ssh = ssh) getOrElse |
|
180 |
error("No repository found in " + start.absolute) |
|
181 |
||
75393 | 182 |
private def make_repository( |
183 |
root: Path, |
|
184 |
cmd: String, |
|
185 |
args: String, |
|
186 |
ssh: SSH.System = SSH.Local |
|
187 |
) : Repository = { |
|
64230 | 188 |
val hg = new Repository(root, ssh) |
72375 | 189 |
ssh.make_directory(hg.root.dir) |
67066 | 190 |
hg.command(cmd, args, repository = false).check |
64168 | 191 |
hg |
192 |
} |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
193 |
|
67065 | 194 |
def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository = |
67066 | 195 |
make_repository(root, "init", ssh.bash_path(root), ssh = ssh) |
67065 | 196 |
|
197 |
def clone_repository(source: String, root: Path, |
|
198 |
rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository = |
|
199 |
make_repository(root, "clone", |
|
67066 | 200 |
options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh) |
67065 | 201 |
|
75393 | 202 |
def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = { |
66570 | 203 |
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
|
204 |
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
|
205 |
} |
64230 | 206 |
|
75393 | 207 |
class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) { |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
208 |
hg => |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
209 |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
210 |
val root: Path = ssh.expand_path(root_path) |
66570 | 211 |
def root_url: String = ssh.hg_url + root.implode |
64230 | 212 |
|
71562 | 213 |
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
|
214 |
|
75393 | 215 |
def command_line( |
216 |
name: String, |
|
217 |
args: String = "", |
|
218 |
options: String = "", |
|
219 |
repository: Boolean = true |
|
220 |
): String = { |
|
73611 | 221 |
"export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + |
222 |
(if (repository) " --repository " + ssh.bash_path(root) else "") + |
|
223 |
" --noninteractive " + name + " " + options + " " + args |
|
224 |
} |
|
225 |
||
226 |
def command( |
|
75393 | 227 |
name: String, |
228 |
args: String = "", |
|
229 |
options: String = "", |
|
230 |
repository: Boolean = true |
|
231 |
): Process_Result = { |
|
73611 | 232 |
ssh.execute(command_line(name, args = args, options = options, repository = repository)) |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
233 |
} |
63999 | 234 |
|
67068 | 235 |
def add(files: List[Path]): Unit = |
71601 | 236 |
hg.command("add", files.map(ssh.bash_path).mkString(" ")) |
67068 | 237 |
|
64505 | 238 |
def archive(target: String, rev: String = "", options: String = ""): Unit = |
239 |
hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check |
|
240 |
||
63999 | 241 |
def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
64168 | 242 |
hg.command("heads", opt_template(template), options).check.out_lines |
63999 | 243 |
|
64232
367d83d6030e
clarified hg.id operation, with explicit tip as default;
wenzelm
parents:
64230
diff
changeset
|
244 |
def identify(rev: String = "tip", options: String = ""): String = |
64168 | 245 |
hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" |
63998 | 246 |
|
64232
367d83d6030e
clarified hg.id operation, with explicit tip as default;
wenzelm
parents:
64230
diff
changeset
|
247 |
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
|
248 |
|
75393 | 249 |
def tags(rev: String = "tip"): String = { |
73524 | 250 |
val result = identify(rev, options = "-t") |
77218 | 251 |
space_explode(' ', result).filterNot(_ == "tip").mkString(" ") |
73524 | 252 |
} |
73521 | 253 |
|
71313 | 254 |
def paths(args: String = "", options: String = ""): List[String] = |
255 |
hg.command("paths", args = args, options = options).check.out_lines |
|
256 |
||
63998 | 257 |
def manifest(rev: String = "", options: String = ""): List[String] = |
64168 | 258 |
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
|
259 |
|
64033 | 260 |
def log(rev: String = "", template: String = "", options: String = ""): String = |
64168 | 261 |
hg.command("log", opt_rev(rev) + opt_template(template), options).check.out |
64027 | 262 |
|
75514 | 263 |
def diff(rev: String = "", options: String = ""): String = |
264 |
hg.command("diff", opt_rev(rev), options).check.out |
|
265 |
||
67755 | 266 |
def parent(): String = log(rev = "p1()", template = "{node|short}") |
267 |
||
73340 | 268 |
def push( |
75393 | 269 |
remote: String = "", |
270 |
rev: String = "", |
|
271 |
force: Boolean = false, |
|
272 |
options: String = "" |
|
273 |
): Unit = { |
|
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
|
274 |
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
|
275 |
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
|
276 |
} |
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
|
277 |
|
63999 | 278 |
def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
64168 | 279 |
hg.command("pull", opt_rev(rev) + optional(remote), options).check |
63999 | 280 |
|
64168 | 281 |
def update( |
75393 | 282 |
rev: String = "", |
283 |
clean: Boolean = false, |
|
284 |
check: Boolean = false, |
|
285 |
options: String = "" |
|
286 |
): Unit = { |
|
64168 | 287 |
hg.command("update", |
288 |
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check |
|
63999 | 289 |
} |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
290 |
|
75470 | 291 |
def status(options: String = ""): List[String] = |
292 |
hg.command("status", options = options).check.out_lines |
|
293 |
||
294 |
def known_files(): List[String] = status(options = "--modified --added --clean --no-status") |
|
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
295 |
|
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
296 |
def sync(context: Rsync.Context, target: String, |
75487 | 297 |
thorough: Boolean = false, |
75474 | 298 |
dry_run: Boolean = false, |
75477 | 299 |
filter: List[String] = Nil, |
75511 | 300 |
contents: List[File.Content] = Nil, |
75479 | 301 |
rev: String = "" |
75474 | 302 |
): Unit = { |
75480 | 303 |
require(ssh == SSH.Local, "local repository required") |
304 |
||
75491 | 305 |
Isabelle_System.with_tmp_dir("sync") { tmp_dir => |
75537
fbe27a50706b
avoid noise via context.progress (amending 68162e4f60a7);
wenzelm
parents:
75535
diff
changeset
|
306 |
val context0 = context.copy(progress = new Progress) |
fbe27a50706b
avoid noise via context.progress (amending 68162e4f60a7);
wenzelm
parents:
75535
diff
changeset
|
307 |
|
fbe27a50706b
avoid noise via context.progress (amending 68162e4f60a7);
wenzelm
parents:
75535
diff
changeset
|
308 |
Rsync.init(context0, target) |
75511 | 309 |
|
310 |
val list = |
|
76617 | 311 |
Rsync.exec(context0, list = true, args = List("--", Url.direct_path(target))) |
75535 | 312 |
.check.out_lines.filterNot(_.endsWith(" .")) |
75514 | 313 |
if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { |
75511 | 314 |
error("No .hg_sync meta data in " + quote(target)) |
315 |
} |
|
316 |
||
75514 | 317 |
val id_content = id(rev = rev) |
318 |
val is_changed = id_content.endsWith("+") |
|
319 |
val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") |
|
320 |
val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" |
|
321 |
val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" |
|
322 |
||
75537
fbe27a50706b
avoid noise via context.progress (amending 68162e4f60a7);
wenzelm
parents:
75535
diff
changeset
|
323 |
Rsync.init(context0, target, |
75514 | 324 |
contents = |
75824 | 325 |
File.content(Hg_Sync.PATH_ID, id_content) :: |
326 |
File.content(Hg_Sync.PATH_LOG, log_content) :: |
|
327 |
File.content(Hg_Sync.PATH_DIFF, diff_content) :: |
|
328 |
File.content(Hg_Sync.PATH_STAT, stat_content) :: contents) |
|
75511 | 329 |
|
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
330 |
val (exclude, source) = |
75479 | 331 |
if (rev.isEmpty) { |
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
332 |
val exclude = ".hg" :: status(options = "--unknown --ignored --no-status") |
75480 | 333 |
val source = File.standard_path(root) |
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
334 |
(exclude, source) |
75479 | 335 |
} |
336 |
else { |
|
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
337 |
val exclude = List(".hg_archival.txt") |
75479 | 338 |
val source = File.standard_path(tmp_dir + Path.explode("archive")) |
339 |
archive(source, rev = rev) |
|
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
340 |
(exclude, source) |
75479 | 341 |
} |
75511 | 342 |
|
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
343 |
val exclude_path = tmp_dir + Path.explode("exclude") |
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
344 |
File.write(exclude_path, cat_lines(exclude.map("/" + _))) |
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
345 |
|
75511 | 346 |
val protect = |
75514 | 347 |
(Hg_Sync.PATH :: contents.map(_.path)) |
348 |
.map(path => "protect /" + File.standard_path(path)) |
|
75526 | 349 |
Rsync.exec(context, |
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
350 |
thorough = thorough, |
75511 | 351 |
dry_run = dry_run, |
352 |
clean = true, |
|
353 |
prune_empty_dirs = true, |
|
354 |
filter = protect ::: filter, |
|
75519
931c48756b88
avoid redundant meta data: exclude .hg_archival.txt;
wenzelm
parents:
75514
diff
changeset
|
355 |
args = List("--exclude-from=" + exclude_path.implode, "--", |
76617 | 356 |
Url.direct_path(source), target) |
75507 | 357 |
).check |
75474 | 358 |
} |
359 |
} |
|
360 |
||
75393 | 361 |
def graph(): Graph = { |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
362 |
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
|
363 |
val log_result = |
65825
11f87ab51ddb
more robust command invocation, without defaults from hgrc;
wenzelm
parents:
65822
diff
changeset
|
364 |
log(template = """node: {node|short} {p1node|short} {p2node|short}\n""") |
73359 | 365 |
split_lines(log_result).foldLeft(Graph.string[Unit]) { |
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
366 |
case (graph, Node(x, y, z)) => |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
367 |
val deps = List(y, z).filterNot(s => s.forall(_ == '0')) |
73359 | 368 |
val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ())) |
369 |
deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) }) |
|
65819
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
370 |
case (graph, _) => graph |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
371 |
} |
ff3dc9325eaa
explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents:
65818
diff
changeset
|
372 |
} |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
373 |
} |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
374 |
|
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
375 |
|
75472 | 376 |
|
377 |
/** check files **/ |
|
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
378 |
|
75393 | 379 |
def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = { |
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
380 |
val outside = new mutable.ListBuffer[Path] |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
381 |
val unknown = new mutable.ListBuffer[Path] |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
382 |
|
75393 | 383 |
@tailrec def check(paths: List[Path]): Unit = { |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
384 |
paths match { |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
385 |
case path :: rest => |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
386 |
find_repository(path, ssh) match { |
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
387 |
case None => outside += path; check(rest) |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
388 |
case Some(hg) => |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
389 |
val known = |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
390 |
hg.known_files().iterator.map(name => |
65833 | 391 |
(hg.root + Path.explode(name)).canonical_file).toSet |
392 |
if (!known(path.canonical_file)) unknown += path |
|
393 |
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
|
394 |
} |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
395 |
case Nil => |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
396 |
} |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
397 |
} |
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
398 |
|
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
399 |
check(files) |
67782
7e223a05e6d8
clarified notion of unknown files: ignore files outside of a Mercurial repository;
wenzelm
parents:
67755
diff
changeset
|
400 |
(outside.toList, unknown.toList) |
65832
2fb85623c386
implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents:
65825
diff
changeset
|
401 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
402 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
403 |
|
75472 | 404 |
|
405 |
/** hg_setup **/ |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
406 |
|
75393 | 407 |
private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = { |
71313 | 408 |
val hgrc = local_hg.root + Path.explode(".hg/hgrc") |
409 |
def header(line: String): Boolean = line.startsWith("[paths]") |
|
410 |
val Entry = """^(\S+)\s*=\s*(.*)$""".r |
|
411 |
val new_entry = path_name + " = " + source |
|
412 |
||
75393 | 413 |
def commit(lines: List[String]): Boolean = { |
71320 | 414 |
File.write(hgrc, cat_lines(lines)) |
71313 | 415 |
true |
416 |
} |
|
417 |
val edited = |
|
418 |
hgrc.is_file && { |
|
419 |
val lines = split_lines(File.read(hgrc)) |
|
71383 | 420 |
lines.count(header) == 1 && { |
71313 | 421 |
if (local_hg.paths(options = "-q").contains(path_name)) { |
422 |
val old_source = local_hg.paths(args = path_name).head |
|
71320 | 423 |
val old_entry = path_name + ".old = " + old_source |
71313 | 424 |
val lines1 = |
425 |
lines.map { |
|
71320 | 426 |
case Entry(a, b) if a == path_name && b == old_source => |
427 |
new_entry + "\n" + old_entry |
|
71313 | 428 |
case line => line |
429 |
} |
|
430 |
lines != lines1 && commit(lines1) |
|
431 |
} |
|
432 |
else { |
|
433 |
val prefix = lines.takeWhile(line => !header(line)) |
|
434 |
val n = prefix.length |
|
435 |
commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1)) |
|
436 |
} |
|
437 |
} |
|
438 |
} |
|
439 |
if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n") |
|
440 |
} |
|
441 |
||
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
442 |
val default_path_name = "default" |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
443 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
444 |
def hg_setup( |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
445 |
remote: String, |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
446 |
local_path: Path, |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
447 |
remote_name: String = "", |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
448 |
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
|
449 |
remote_exists: Boolean = false, |
75393 | 450 |
progress: Progress = new Progress |
451 |
): Unit = { |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
452 |
/* local repository */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
453 |
|
72375 | 454 |
Isabelle_System.make_directory(local_path) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
455 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
456 |
val repos_name = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
457 |
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
|
458 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
459 |
val local_hg = |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
460 |
if (is_repository(local_path)) repository(local_path) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
461 |
else init_repository(local_path) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
462 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
463 |
progress.echo("Local repository " + local_hg.root.absolute) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
464 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
465 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
466 |
/* remote repository */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
467 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
468 |
val remote_url = { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
469 |
if (remote.startsWith("ssh://")) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
470 |
val ssh_url = remote + "/" + repos_name |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
471 |
|
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
472 |
if (!remote_exists) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
473 |
try { local_hg.command("init", ssh_url, repository = false).check } |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
474 |
catch { case ERROR(msg) => progress.echo_warning(msg) } |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
475 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
476 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
477 |
ssh_url |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
478 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
479 |
else { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
480 |
val phabricator = Phabricator.API(remote) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
481 |
|
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
482 |
var repos = |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
483 |
phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
484 |
if (remote_exists) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
485 |
error("Remote repository " + |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
486 |
quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist") |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
487 |
} |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
488 |
else phabricator.create_repository(repos_name, short_name = repos_name) |
71321
edf3210a61a2
added option -r: support more robust consolidation of local clones with varying names;
wenzelm
parents:
71320
diff
changeset
|
489 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
490 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
491 |
while (repos.importing) { |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
492 |
progress.echo("Awaiting remote repository ...") |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
493 |
Time.seconds(0.5).sleep() |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
494 |
repos = phabricator.the_repository(repos.phid) |
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
495 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
496 |
|
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
497 |
repos.ssh_url |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
498 |
} |
76169
a3c694039fd6
discontinued pointless SSH.Target: OpenSSH client can handle user@host directly;
wenzelm
parents:
76136
diff
changeset
|
499 |
} |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
500 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
501 |
progress.echo("Remote repository " + quote(remote_url)) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
502 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
503 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
504 |
/* synchronize local and remote state */ |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
505 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
506 |
progress.echo("Synchronizing ...") |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
507 |
|
71313 | 508 |
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
|
509 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
510 |
local_hg.pull(options = "-u") |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
511 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
512 |
local_hg.push(remote = remote_url) |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
513 |
} |
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
514 |
|
75474 | 515 |
val isabelle_tool1 = |
72763 | 516 |
Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository", |
75394 | 517 |
Scala_Project.here, |
518 |
{ args => |
|
519 |
var remote_name = "" |
|
520 |
var path_name = default_path_name |
|
521 |
var remote_exists = false |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
522 |
|
75394 | 523 |
val getopts = Getopts(""" |
71322 | 524 |
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
|
525 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
526 |
Options are: |
71322 | 527 |
-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
|
528 |
-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
|
529 |
-r assume that remote repository already exists |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
530 |
|
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
531 |
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
|
532 |
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
|
533 |
""", |
75394 | 534 |
"n:" -> (arg => remote_name = arg), |
535 |
"p:" -> (arg => path_name = arg), |
|
536 |
"r" -> (_ => remote_exists = true)) |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
537 |
|
75394 | 538 |
val more_args = getopts(args) |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
539 |
|
75394 | 540 |
val (remote, local_path) = |
541 |
more_args match { |
|
542 |
case List(arg1, arg2) => (arg1, Path.explode(arg2)) |
|
543 |
case _ => getopts.usage() |
|
544 |
} |
|
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
545 |
|
75394 | 546 |
val progress = new Console_Progress |
71312
937328d61436
added command hg_setup: setup remote vs. local Mercurial repository;
wenzelm
parents:
68566
diff
changeset
|
547 |
|
75394 | 548 |
hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name, |
549 |
remote_exists = remote_exists, progress = progress) |
|
550 |
}) |
|
75474 | 551 |
|
552 |
||
553 |
||
554 |
/** hg_sync **/ |
|
555 |
||
556 |
val isabelle_tool2 = |
|
75479 | 557 |
Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory", |
75474 | 558 |
Scala_Project.here, { args => |
75489 | 559 |
var filter: List[String] = Nil |
76134 | 560 |
var protect_args = false |
75474 | 561 |
var root: Option[Path] = None |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
562 |
var ssh_control_path = "" |
75487 | 563 |
var thorough = false |
75474 | 564 |
var dry_run = false |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
565 |
var ssh_port = 0 |
75479 | 566 |
var rev = "" |
75474 | 567 |
var verbose = false |
568 |
||
569 |
val getopts = Getopts(""" |
|
570 |
Usage: isabelle hg_sync [OPTIONS] TARGET |
|
571 |
||
572 |
Options are: |
|
75511 | 573 |
-F RULE add rsync filter RULE |
574 |
(e.g. "protect /foo" to avoid deletion) |
|
76134 | 575 |
-P protect spaces in target file names: more robust, less portable |
75474 | 576 |
-R ROOT explicit repository root directory |
577 |
(default: implicit from current directory) |
|
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
578 |
-S PATH SSH control path for connection multiplexing |
75493 | 579 |
-T thorough treatment of file content and directory times |
75474 | 580 |
-n no changes: dry-run |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
581 |
-p PORT SSH port |
75479 | 582 |
-r REV explicit revision (default: state of working directory) |
75474 | 583 |
-v verbose |
584 |
||
75479 | 585 |
Synchronize Mercurial repository with TARGET directory, |
75474 | 586 |
which can be local or remote (using notation of rsync). |
587 |
""", |
|
75489 | 588 |
"F:" -> (arg => filter = filter ::: List(arg)), |
76134 | 589 |
"P" -> (_ => protect_args = true), |
75474 | 590 |
"R:" -> (arg => root = Some(Path.explode(arg))), |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
591 |
"S:" -> (arg => ssh_control_path = arg), |
75487 | 592 |
"T" -> (_ => thorough = true), |
75474 | 593 |
"n" -> (_ => dry_run = true), |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
594 |
"p:" -> (arg => ssh_port = Value.Int.parse(arg)), |
75479 | 595 |
"r:" -> (arg => rev = arg), |
75474 | 596 |
"v" -> (_ => verbose = true)) |
597 |
||
598 |
val more_args = getopts(args) |
|
599 |
val target = |
|
600 |
more_args match { |
|
601 |
case List(target) => target |
|
602 |
case _ => getopts.usage() |
|
603 |
} |
|
604 |
||
77518
fda4da0f80f4
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77368
diff
changeset
|
605 |
val progress = new Console_Progress(verbose = verbose) |
75474 | 606 |
val hg = |
607 |
root match { |
|
608 |
case Some(dir) => repository(dir) |
|
609 |
case None => the_repository(Path.current) |
|
610 |
} |
|
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
611 |
val context = Rsync.Context(progress, ssh_port = ssh_port, |
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76134
diff
changeset
|
612 |
ssh_control_path = ssh_control_path, protect_args = protect_args) |
77518
fda4da0f80f4
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77368
diff
changeset
|
613 |
hg.sync(context, target, thorough = thorough, dry_run = dry_run, filter = filter, rev = rev) |
75474 | 614 |
} |
615 |
) |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
616 |
} |