author | wenzelm |
Tue, 11 Oct 2016 09:37:59 +0200 | |
changeset 64138 | cf0c8c5782af |
parent 64033 | 2989c1f2593a |
child 64162 | 03057a8fdd1f |
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 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
27 |
def open_repository(root: Path): Repository = new Repository(root) |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
28 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
29 |
class Repository private[Mercurial](val root: Path) |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
30 |
{ |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
31 |
override def toString: String = root.toString |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
32 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
33 |
def close() { } |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
34 |
|
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
35 |
def command(cmd: String, cwd: JFile = null): Process_Result = |
64028 | 36 |
Isabelle_System.hg("--repository " + File.bash_path(root) + " --noninteractive " + cmd, |
37 |
cwd = cwd) |
|
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
38 |
|
63999 | 39 |
|
40 |
def heads(template: String = "{node|short}\n", options: String = ""): List[String] = |
|
41 |
command("heads " + options + opt_template(template)).check.out_lines |
|
42 |
||
63998 | 43 |
def identify(rev: String = "", options: String = ""): String = |
64020
355b78441650
clarified: a variant of -i is the default, but its output is not as precise as it might seem;
wenzelm
parents:
63999
diff
changeset
|
44 |
command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse "" |
63998 | 45 |
|
46 |
def manifest(rev: String = "", options: String = ""): List[String] = |
|
47 |
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
|
48 |
|
64033 | 49 |
def log(rev: String = "", template: String = "", options: String = ""): String = |
64138
cf0c8c5782af
eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
wenzelm
parents:
64033
diff
changeset
|
50 |
command("log " + options + opt_rev(rev) + opt_template(template)).check.out |
64027 | 51 |
|
63999 | 52 |
def pull(remote: String = "", rev: String = "", options: String = ""): Unit = |
53 |
command("pull " + options + opt_rev(rev) + optional(remote)).check |
|
54 |
||
55 |
def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "") |
|
56 |
{ |
|
57 |
command("update " + options + |
|
58 |
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check |
|
59 |
} |
|
60 |
||
63997
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
61 |
command("root").check |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
62 |
} |
e11ccb5aa82f
more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff
changeset
|
63 |
} |