23 |
23 |
24 |
24 |
25 /* repository access */ |
25 /* repository access */ |
26 |
26 |
27 def repository(root: Path, ssh: Option[SSH.Session] = None): Repository = |
27 def repository(root: Path, ssh: Option[SSH.Session] = None): Repository = |
28 new Repository(root, ssh) |
28 { |
|
29 val hg = new Repository(root, ssh) |
|
30 hg.command("root").check |
|
31 hg |
|
32 } |
|
33 |
|
34 def clone_repository( |
|
35 source: String, dest: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository = |
|
36 { |
|
37 val hg = new Repository(dest, ssh) |
|
38 hg.command("clone", |
|
39 File.bash_string(source) + " " + File.bash_string(dest.implode), options).check |
|
40 hg |
|
41 } |
29 |
42 |
30 class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session]) |
43 class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session]) |
31 { |
44 { |
32 hg => |
45 hg => |
33 |
46 |
35 ssh match { |
48 ssh match { |
36 case None => root.implode |
49 case None => root.implode |
37 case Some(session) => quote(session.toString + ":" + root.implode) |
50 case Some(session) => quote(session.toString + ":" + root.implode) |
38 } |
51 } |
39 |
52 |
40 def command(cmd: String): Process_Result = |
53 def command(name: String, args: String = "", options: String = ""): Process_Result = |
41 { |
54 { |
42 val cmdline = |
55 val cmdline = |
43 "\"${HG:-hg}\" --repository " + File.bash_string(root.implode) + " --noninteractive " + cmd |
56 "\"${HG:-hg}\"" + |
|
57 (if (name == "clone") "" else " --repository " + File.bash_string(root.implode)) + |
|
58 " --noninteractive " + name + " " + options + " " + args |
44 ssh match { |
59 ssh match { |
45 case None => Isabelle_System.bash(cmdline) |
60 case None => Isabelle_System.bash(cmdline) |
46 case Some(session) => session.execute(cmdline) |
61 case Some(session) => session.execute(cmdline) |
47 } |
62 } |
48 } |
63 } |
49 |
64 |
50 def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
65 def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
51 hg.command("heads " + options + opt_template(template)).check.out_lines |
66 hg.command("heads", opt_template(template), options).check.out_lines |
52 |
67 |
53 def identify(rev: String = "", options: String = ""): String = |
68 def identify(rev: String = "", options: String = ""): String = |
54 hg.command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse "" |
69 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" |
55 |
70 |
56 def manifest(rev: String = "", options: String = ""): List[String] = |
71 def manifest(rev: String = "", options: String = ""): List[String] = |
57 hg.command("manifest " + options + opt_rev(rev)).check.out_lines |
72 hg.command("manifest", opt_rev(rev), options).check.out_lines |
58 |
73 |
59 def log(rev: String = "", template: String = "", options: String = ""): String = |
74 def log(rev: String = "", template: String = "", options: String = ""): String = |
60 hg.command("log " + options + opt_rev(rev) + opt_template(template)).check.out |
75 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out |
61 |
76 |
62 def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
77 def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
63 hg.command("pull " + options + opt_rev(rev) + optional(remote)).check |
78 hg.command("pull", opt_rev(rev) + optional(remote), options).check |
64 |
79 |
65 def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") |
80 def update( |
|
81 rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") |
66 { |
82 { |
67 hg.command("update " + options + |
83 hg.command("update", |
68 opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check |
84 opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check |
69 } |
85 } |
70 |
|
71 hg.command("root").check |
|
72 } |
86 } |
73 } |
87 } |