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