# HG changeset patch # User wenzelm # Date 1654452899 -7200 # Node ID 0c2ff768caf51dd8f7761e1947db1f57baf4cc01 # Parent 36316c6a3fc23667c1c1b9de8346a1d58bba799e more meta data; clarified signature: more explicit types; diff -r 36316c6a3fc2 -r 0c2ff768caf5 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sun Jun 05 20:14:32 2022 +0200 +++ b/src/Pure/General/mercurial.scala Sun Jun 05 20:14:59 2022 +0200 @@ -117,8 +117,36 @@ /* hg_sync meta data */ - val HG_SYNC: Path = Path.explode(".hg_sync") - val HG_SYNC_ID: Path = HG_SYNC + Path.explode("id") + object Hg_Sync { + val NAME = ".hg_sync" + val _NAME: String = " " + NAME + val PATH: Path = Path.explode(NAME) + val PATH_ID: Path = PATH + Path.explode("id") + val PATH_LOG: Path = PATH + Path.explode("log") + val PATH_DIFF: Path = PATH + Path.explode("diff") + val PATH_STAT: Path = PATH + Path.explode("stat") + + def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = + ssh.is_dir(root + PATH) + + def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = { + if (is_directory(root, ssh = ssh)) new Directory(root, ssh) + else error("No .hg_sync directory found in " + ssh.rsync_path(root)) + } + + class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System) + { + override def toString: String = ssh.rsync_path(root) + + def read(path: Path): String = ssh.read(root + path) + lazy val id: String = read(PATH_ID) + lazy val log: String = read(PATH_LOG) + lazy val diff: String = read(PATH_DIFF) + lazy val stat: String = read(PATH_STAT) + + def changed: Boolean = id.endsWith("+") + } + } /* repository access */ @@ -232,6 +260,9 @@ def log(rev: String = "", template: String = "", options: String = ""): String = hg.command("log", opt_rev(rev) + opt_template(template), options).check.out + def diff(rev: String = "", options: String = ""): String = + hg.command("diff", opt_rev(rev), options).check.out + def parent(): String = log(rev = "p1()", template = "{node|short}") def push( @@ -281,12 +312,22 @@ Isabelle_System.rsync(port = port, list = true, args = List("--", Isabelle_System.rsync_dir(target)) ).check.out_lines.filterNot(_.endsWith(" .")) - if (list.nonEmpty && !list.exists(_.endsWith(" .hg_sync"))) { + if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) { error("No .hg_sync meta data in " + quote(target)) } + val id_content = id(rev = rev) + val is_changed = id_content.endsWith("+") + val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") + val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" + val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" + Isabelle_System.rsync_init(target, port = port, - contents = File.Content(HG_SYNC_ID, id(rev = rev)) :: contents) + contents = + File.Content(Hg_Sync.PATH_ID, id_content) :: + File.Content(Hg_Sync.PATH_LOG, log_content) :: + File.Content(Hg_Sync.PATH_DIFF, diff_content) :: + File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents) val (options, source) = if (rev.isEmpty) { @@ -305,7 +346,8 @@ } val protect = - (HG_SYNC :: contents.map(_.path)).map(path => "protect /" + File.standard_path(path)) + (Hg_Sync.PATH :: contents.map(_.path)) + .map(path => "protect /" + File.standard_path(path)) Isabelle_System.rsync( progress = progress, port = port, verbose = verbose, thorough = thorough, dry_run = dry_run,