author | wenzelm |
Sun, 11 Dec 2022 12:52:46 +0100 | |
changeset 76617 | d5adc9126ae8 |
parent 76616 | e6c11ef4fb51 |
child 77369 | df17355f1e2c |
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 { |
|
75527 | 11 |
sealed case class Context(progress: Progress, |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
12 |
ssh_port: Int = 0, |
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
13 |
ssh_control_path: String = "", |
75527 | 14 |
archive: Boolean = true, |
75554 | 15 |
protect_args: Boolean = true // requires rsync 3.0.0, or later |
75527 | 16 |
) { |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
17 |
def command: String = { |
76170 | 18 |
val ssh_command = SSH.client_command(port = ssh_port, control_path = ssh_control_path) |
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
19 |
"rsync --rsh=" + Bash.string(ssh_command) + |
75527 | 20 |
(if (archive) " --archive" else "") + |
21 |
(if (protect_args) " --protect-args" else "") |
|
76136
1bb677cceea4
let rsync re-use ssh connection via control path;
wenzelm
parents:
76131
diff
changeset
|
22 |
} |
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
23 |
} |
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
24 |
|
75526 | 25 |
def exec( |
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
26 |
context: Context, |
75523 | 27 |
verbose: Boolean = false, |
28 |
thorough: Boolean = false, |
|
29 |
prune_empty_dirs: Boolean = false, |
|
30 |
dry_run: Boolean = false, |
|
31 |
clean: Boolean = false, |
|
32 |
list: Boolean = false, |
|
33 |
filter: List[String] = Nil, |
|
34 |
args: List[String] = Nil |
|
35 |
): Process_Result = { |
|
36 |
val script = |
|
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
37 |
context.command + |
75523 | 38 |
(if (verbose) " --verbose" else "") + |
39 |
(if (thorough) " --ignore-times" else " --omit-dir-times") + |
|
40 |
(if (prune_empty_dirs) " --prune-empty-dirs" else "") + |
|
41 |
(if (dry_run) " --dry-run" else "") + |
|
42 |
(if (clean) " --delete-excluded" else "") + |
|
43 |
(if (list) " --list-only --no-human-readable" else "") + |
|
44 |
filter.map(s => " --filter=" + Bash.string(s)).mkString + |
|
45 |
(if (args.nonEmpty) " " + Bash.strings(args) else "") |
|
75525
68162e4f60a7
clarified signature: more explicit type Rsync.Context;
wenzelm
parents:
75524
diff
changeset
|
46 |
context.progress.bash(script, echo = true) |
75523 | 47 |
} |
48 |
||
75526 | 49 |
def init(context: Context, target: String, |
75523 | 50 |
contents: List[File.Content] = Nil |
51 |
): Unit = |
|
52 |
Isabelle_System.with_tmp_dir("sync") { tmp_dir => |
|
53 |
val init_dir = Isabelle_System.make_directory(tmp_dir + Path.explode("init")) |
|
54 |
contents.foreach(_.write(init_dir)) |
|
75534
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
55 |
exec(context.copy(archive = false), |
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
56 |
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
|
57 |
args = |
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
58 |
List(if (contents.nonEmpty) "--archive" else "--dirs", |
1d937b12204d
more robust: no change of directory attributes of initial test, notably target without .hg_sync meta data;
wenzelm
parents:
75527
diff
changeset
|
59 |
File.bash_path(init_dir) + "/.", target)).check |
75523 | 60 |
} |
61 |
} |