author | wenzelm |
Sat, 08 Apr 2023 17:20:15 +0200 | |
changeset 77787 | b20ac2c26ea3 |
parent 77785 | 721b3278c8e4 |
child 77788 | c2ce9ac85859 |
permissions | -rw-r--r-- |
75523 | 1 |
/* Title: Pure/General/rsync.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for rsync: see also https://rsync.samba.org |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Rsync { |
|
77787 | 11 |
object Context { |
12 |
def apply( |
|
13 |
progress: Progress = new Progress, |
|
14 |
ssh: SSH.System = SSH.Local, |
|
15 |
archive: Boolean = true, |
|
16 |
protect_args: Boolean = true // requires rsync 3.0.0, or later |
|
17 |
): Context = new Context(progress, ssh, archive, protect_args) |
|
18 |
} |
|
19 |
||
20 |
final class Context private( |
|
21 |
val progress: Progress, |
|
22 |
val ssh: SSH.System, |
|
23 |
archive: Boolean, |
|
24 |
protect_args: Boolean |
|
75527 | 25 |
) { |
77787 | 26 |
def no_progress: Context = new Context(new Progress, ssh, archive, protect_args) |
27 |
def no_archive: Context = new Context(progress, ssh, false, protect_args) |
|
28 |
||
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
29 |
def command: String = { |
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
30 |
val ssh_command = ssh.client_command |
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
31 |
"rsync" + |
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
32 |
if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) + |
75527 | 33 |
(if (archive) " --archive" else "") + |
34 |
(if (protect_args) " --protect-args" else "") |
|
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
35 |
} |
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
36 |
|
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
37 |
def target(path: Path, direct: Boolean = false): String = { |
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
38 |
val s = ssh.rsync_path(path) |
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
39 |
if (direct) Url.direct_path(s) else s |
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
40 |
} |
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
41 |
} |
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
42 |
|
75526 | 43 |
def exec( |
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
44 |
context: Context, |
75523 | 45 |
thorough: Boolean = false, |
46 |
prune_empty_dirs: Boolean = false, |
|
47 |
dry_run: Boolean = false, |
|
48 |
clean: Boolean = false, |
|
49 |
filter: List[String] = Nil, |
|
50 |
args: List[String] = Nil |
|
51 |
): Process_Result = { |
|
77517 | 52 |
val progress = context.progress |
75523 | 53 |
val script = |
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
54 |
context.command + |
77518
fda4da0f80f4
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77517
diff
changeset
|
55 |
(if (progress.verbose) " --verbose" else "") + |
75523 | 56 |
(if (thorough) " --ignore-times" else " --omit-dir-times") + |
57 |
(if (prune_empty_dirs) " --prune-empty-dirs" else "") + |
|
58 |
(if (dry_run) " --dry-run" else "") + |
|
59 |
(if (clean) " --delete-excluded" else "") + |
|
60 |
filter.map(s => " --filter=" + Bash.string(s)).mkString + |
|
77369 | 61 |
if_proper(args, " " + Bash.strings(args)) |
77517 | 62 |
progress.bash(script, echo = true) |
75523 | 63 |
} |
64 |
||
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
65 |
def init(context: Context, target: Path, |
75523 | 66 |
contents: List[File.Content] = Nil |
67 |
): Unit = |
|
68 |
Isabelle_System.with_tmp_dir("sync") { tmp_dir => |
|
69 |
val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init")) |
|
70 |
contents.foreach(_.write(init_dir)) |
|
77787 | 71 |
exec(context.no_archive, |
75534
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
72 |
thorough = true, |
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
73 |
args = |
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
74 |
List(if (contents.nonEmpty) "--archive" else "--dirs", |
77783
fb61887c069a
clarified underlying SSH session of "isabelle hg_sync" and "isabelle sync";
wenzelm
parents:
77518
diff
changeset
|
75 |
File.bash_path(init_dir) + "/.", context.target(target))).check |
75523 | 76 |
} |
77 |
} |