author | wenzelm |
Wed, 12 Oct 2016 15:23:54 +0200 | |
changeset 64167 | 097d122222f6 |
parent 64162 | 03057a8fdd1f |
child 64168 | e573b985390c |
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 = |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
28 |
new Repository(root, ssh) |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
29 |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
30 |
class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session]) |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
31 |
{ |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
32 |
hg => |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
33 |
|
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
34 |
override def toString: String = |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
35 |
ssh match { |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
36 |
case None => root.implode |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
37 |
case Some(session) => quote(session.toString + ":" + root.implode) |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
38 |
} |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
39 |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
40 |
def command(cmd: String): Process_Result = |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
41 |
{ |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
42 |
val cmdline = |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
43 |
"\"${HG:-hg}\" --repository " + File.bash_string(root.implode) + " --noninteractive " + cmd |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
44 |
ssh match { |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
45 |
case None => Isabelle_System.bash(cmdline) |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
46 |
case Some(session) => session.execute(cmdline) |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
47 |
} |
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
48 |
} |
63999 | 49 |
|
50 |
def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
51 |
hg.command("heads " + options + opt_template(template)).check.out_lines |
63999 | 52 |
|
63998 | 53 |
def identify(rev: String = "", options: String = ""): String = |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
54 |
hg.command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse "" |
63998 | 55 |
|
56 |
def manifest(rev: String = "", options: String = ""): List[String] = |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
57 |
hg.command("manifest " + options + opt_rev(rev)).check.out_lines |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
58 |
|
64033 | 59 |
def log(rev: String = "", template: String = "", options: String = ""): String = |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
60 |
hg.command("log " + options + opt_rev(rev) + opt_template(template)).check.out |
64027 | 61 |
|
63999 | 62 |
def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
63 |
hg.command("pull " + options + opt_rev(rev) + optional(remote)).check |
63999 | 64 |
|
65 |
def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") |
|
66 |
{ |
|
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
67 |
hg.command("update " + options + |
63999 | 68 |
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check |
69 |
} |
|
70 |
||
64167
097d122222f6
support remote repositories via ssh command execution;
wenzelm
parents:
64162
diff
changeset
|
71 |
hg.command("root").check |
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
72 |
} |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
73 |
} |