1/*  Title:      Pure/General/mercurial.scala
2    Author:     Makarius
3
4Support for Mercurial repositories, with local or remote repository clone
5and working directory (via ssh connection).
6*/
7
8package isabelle
9
10
11import java.io.{File => JFile}
12
13import scala.annotation.tailrec
14import scala.collection.mutable
15
16
17object Mercurial
18{
19  type Graph = isabelle.Graph[String, Unit]
20
21
22  /* command-line syntax */
23
24  def optional(s: String, prefix: String = ""): String =
25    if (s == "") "" else " " + prefix + " " + Bash.string(s)
26
27  def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
28  def opt_rev(s: String): String = optional(s, "--rev")
29  def opt_template(s: String): String = optional(s, "--template")
30
31
32  /* repository access */
33
34  def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
35    ssh.is_dir(root + Path.explode(".hg")) &&
36    new Repository(root, ssh).command("root").ok
37
38  def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
39  {
40    val hg = new Repository(root, ssh)
41    hg.command("root").check
42    hg
43  }
44
45  def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
46  {
47    def find(root: Path): Option[Repository] =
48      if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
49      else if (root.is_root) None
50      else find(root + Path.parent)
51
52    find(ssh.expand_path(start))
53  }
54
55  private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
56    : Repository =
57  {
58    val hg = new Repository(root, ssh)
59    ssh.mkdirs(hg.root.dir)
60    hg.command(cmd, args, repository = false).check
61    hg
62  }
63
64  def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
65    make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
66
67  def clone_repository(source: String, root: Path,
68      rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
69    make_repository(root, "clone",
70      options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
71
72  def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
73  {
74    if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
75    else clone_repository(source, root, options = "--noupdate", ssh = ssh)
76  }
77
78  class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
79  {
80    hg =>
81
82    val root = ssh.expand_path(root_path)
83    def root_url: String = ssh.hg_url + root.implode
84
85    override def toString: String = ssh.prefix + root.implode
86
87    def command(name: String, args: String = "", options: String = "",
88      repository: Boolean = true): Process_Result =
89    {
90      val cmdline =
91        "export HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
92          (if (repository) " --repository " + ssh.bash_path(root) else "") +
93          " --noninteractive " + name + " " + options + " " + args
94      ssh.execute(cmdline)
95    }
96
97    def add(files: List[Path]): Unit =
98      hg.command("add", files.map(ssh.bash_path(_)).mkString(" "))
99
100    def archive(target: String, rev: String = "", options: String = ""): Unit =
101      hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
102
103    def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
104      hg.command("heads", opt_template(template), options).check.out_lines
105
106    def identify(rev: String = "tip", options: String = ""): String =
107      hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
108
109    def id(rev: String = "tip"): String = identify(rev, options = "-i")
110
111    def manifest(rev: String = "", options: String = ""): List[String] =
112      hg.command("manifest", opt_rev(rev), options).check.out_lines
113
114    def log(rev: String = "", template: String = "", options: String = ""): String =
115      hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
116
117    def parent(): String = log(rev = "p1()", template = "{node|short}")
118
119    def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "")
120    {
121      hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
122        check_rc(rc => rc == 0 | rc == 1)
123    }
124
125    def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
126      hg.command("pull", opt_rev(rev) + optional(remote), options).check
127
128    def update(
129      rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
130    {
131      hg.command("update",
132        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
133    }
134
135    def known_files(): List[String] =
136      hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
137
138    def graph(): Graph =
139    {
140      val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
141      val log_result =
142        log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
143      (Graph.string[Unit] /: split_lines(log_result)) {
144        case (graph, Node(x, y, z)) =>
145          val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
146          val graph1 = (graph /: (x :: deps))(_.default_node(_, ()))
147          (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) })
148        case (graph, _) => graph
149      }
150    }
151  }
152
153
154  /* check files */
155
156  def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) =
157  {
158    val outside = new mutable.ListBuffer[Path]
159    val unknown = new mutable.ListBuffer[Path]
160
161    @tailrec def check(paths: List[Path])
162    {
163      paths match {
164        case path :: rest =>
165          find_repository(path, ssh) match {
166            case None => outside += path; check(rest)
167            case Some(hg) =>
168              val known =
169                hg.known_files().iterator.map(name =>
170                  (hg.root + Path.explode(name)).canonical_file).toSet
171              if (!known(path.canonical_file)) unknown += path
172              check(rest.filterNot(p => known(p.canonical_file)))
173          }
174        case Nil =>
175      }
176    }
177
178    check(files)
179    (outside.toList, unknown.toList)
180  }
181}
182