author | wenzelm |
Sat, 15 Oct 2016 20:51:41 +0200 | |
changeset 64230 | 13a97c1d7d22 |
parent 64198 | 351b8211aef9 |
child 64232 | 367d83d6030e |
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 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
4 |
Support for Mercurial repositories. |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
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 |
package isabelle |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
8 |
|
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 |
import java.io.{File => JFile} |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
11 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
12 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
13 |
object Mercurial |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
14 |
{ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
15 |
/* command-line syntax */ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
16 |
|
63999 | 17 |
def optional(s: String, prefix: String = ""): String = |
18 |
if (s == "") "" else " " + prefix + " " + File.bash_string(s) |
|
19 |
||
20 |
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else "" |
|
21 |
def opt_rev(s: String): String = optional(s, "--rev") |
|
22 |
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
|
23 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
24 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
25 |
/* repository access */ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
26 |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
27 |
def repository(root: Path, ssh: Option[SSH.Session] = None): Repository = |
64168 | 28 |
{ |
29 |
val hg = new Repository(root, ssh) |
|
30 |
hg.command("root").check |
|
31 |
hg |
|
32 |
} |
|
33 |
||
34 |
def clone_repository( |
|
64230 | 35 |
source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository = |
64168 | 36 |
{ |
64230 | 37 |
val hg = new Repository(root, ssh) |
38 |
hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check |
|
64168 | 39 |
hg |
40 |
} |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
41 |
|
64230 | 42 |
def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository = |
43 |
ssh match { |
|
44 |
case None => if (root.is_dir) repository(root) else clone_repository(source, root) |
|
45 |
case Some(session) => |
|
46 |
using(session.sftp())(sftp => |
|
47 |
if (sftp.is_dir(sftp.path(root))) repository(root, ssh = ssh) |
|
48 |
else clone_repository(source, root, ssh = ssh)) |
|
49 |
} |
|
50 |
||
51 |
class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session]) |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
52 |
{ |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
53 |
hg => |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
54 |
|
64230 | 55 |
val root = |
56 |
ssh match { |
|
57 |
case None => root_path.expand |
|
58 |
case Some(session) => using(session.sftp())(sftp => root_path.expand_env(sftp.settings)) |
|
59 |
} |
|
60 |
||
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
61 |
override def toString: String = |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
62 |
ssh match { |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
63 |
case None => root.implode |
64169 | 64 |
case Some(session) => session.toString + ":" + root.implode |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
65 |
} |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
66 |
|
64168 | 67 |
def command(name: String, args: String = "", options: String = ""): Process_Result = |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
68 |
{ |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
69 |
val cmdline = |
64168 | 70 |
"\"${HG:-hg}\"" + |
64230 | 71 |
(if (name == "clone") "" else " --repository " + File.bash_path(root)) + |
64168 | 72 |
" --noninteractive " + name + " " + options + " " + args |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
73 |
ssh match { |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
74 |
case None => Isabelle_System.bash(cmdline) |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
75 |
case Some(session) => session.execute(cmdline) |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
76 |
} |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
77 |
} |
63999 | 78 |
|
79 |
def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
|
64168 | 80 |
hg.command("heads", opt_template(template), options).check.out_lines |
63999 | 81 |
|
63998 | 82 |
def identify(rev: String = "", options: String = ""): String = |
64168 | 83 |
hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse "" |
63998 | 84 |
|
85 |
def manifest(rev: String = "", options: String = ""): List[String] = |
|
64168 | 86 |
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
|
87 |
|
64033 | 88 |
def log(rev: String = "", template: String = "", options: String = ""): String = |
64168 | 89 |
hg.command("log", opt_rev(rev) + opt_template(template), options).check.out |
64027 | 90 |
|
63999 | 91 |
def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
64168 | 92 |
hg.command("pull", opt_rev(rev) + optional(remote), options).check |
63999 | 93 |
|
64198 | 94 |
def pull_id(remote: String = ""): String = |
95 |
{ |
|
96 |
hg.pull(remote = remote, options = "-q") |
|
97 |
hg.identify("tip", options = "-i") |
|
98 |
} |
|
99 |
||
64168 | 100 |
def update( |
101 |
rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") |
|
63999 | 102 |
{ |
64168 | 103 |
hg.command("update", |
104 |
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check |
|
63999 | 105 |
} |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
106 |
} |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
107 |
} |