# HG changeset patch
# User wenzelm
# Date 1653850630 -7200
# Node ID 4363ad65ad361f66ced76c13feb3d72d5180ba29
# Parent  904607aedc4b38ebeb714849eb62bf54c87a6afb
support option -r;

diff -r 904607aedc4b -r 4363ad65ad36 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sun May 29 17:37:43 2022 +0200
+++ b/src/Doc/System/Misc.thy	Sun May 29 20:57:10 2022 +0200
@@ -303,9 +303,9 @@
 section \<open>Mercurial repository synchronization\<close>
 
 text \<open>
-  The @{tool_def hg_sync} tool synchronizes the working directory of a local
-  Mercurial repository with a target directory, using
-  \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for destinations.
+  The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
+  a target directory, using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close>
+  notation for destinations.
 
   @{verbatim [display]
 \<open>Usage: isabelle hg_sync [OPTIONS] TARGET
@@ -318,15 +318,19 @@
                  (default: implicit from current directory)
     -f           force changes: no dry-run
     -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
     -v           verbose
 
-  Synchronize Mercurial repository working directory with other TARGET,
+  Synchronize Mercurial repository with TARGET directory,
   which can be local or remote (using notation of rsync).\<close>}
 
   The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
   using \<^verbatim>\<open>rsync\<close> notation (see examples below). The content is written
   directly into the target, \<^emph>\<open>without\<close> creating a separate sub-directory.
 
+  \<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
+  is the current state of the working directory (which might be uncommitted).
+
   \<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode:
   operations are only simulated and printed as in verbose mode. Option \<^verbatim>\<open>-f\<close>
   disables ``dry-run'' mode and thus forces changes to be applied.
@@ -341,8 +345,8 @@
   \<^verbatim>\<open>-P\<close> options may be given to accumulate protected entries.
 
   \<^medskip> Option \<^verbatim>\<open>-R\<close> specifies an explicit repository root directory. The default
-  is to derive it from the current working directory, searching upwards until
-  a suitable \<^verbatim>\<open>.hg\<close> directory is found.
+  is to derive it from the current directory, searching upwards until a
+  suitable \<^verbatim>\<open>.hg\<close> directory is found.
 \<close>
 
 subsubsection \<open>Examples\<close>
diff -r 904607aedc4b -r 4363ad65ad36 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun May 29 17:37:43 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 29 20:57:10 2022 +0200
@@ -257,17 +257,27 @@
       dry_run: Boolean = false,
       clean: Boolean = false,
       filter: List[String] = Nil,
+      rev: String = ""
     ): Unit = {
       Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
-        val exclude_path = tmp_dir + Path.explode("exclude")
-        val exclude = status(options = "--unknown --ignored --no-status")
-        File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
+        val (options, source) =
+          if (rev.isEmpty) {
+            val exclude_path = tmp_dir + Path.explode("exclude")
+            val exclude = status(options = "--unknown --ignored --no-status")
+            File.write(exclude_path, cat_lines((".hg" :: exclude).map("/" + _)))
 
-        val options = List("--exclude-from=" + exclude_path.implode)
-        val source = ssh.rsync_url + root.expand.implode + "/."
+            val options = List("--exclude-from=" + exclude_path.implode)
+            val source = ssh.rsync_url + root.expand.implode
+            (options, source)
+          }
+          else {
+            val source = File.standard_path(tmp_dir + Path.explode("archive"))
+            archive(source, rev = rev)
+            (Nil, source)
+          }
         Isabelle_System.rsync(
           progress = progress, verbose = verbose, dry_run = dry_run, clean = clean, filter = filter,
-          args = List("--prune-empty-dirs") ::: options ::: List("--", source, target)).check
+          args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target)).check
       }
     }
 
@@ -469,12 +479,13 @@
   /** hg_sync **/
 
   val isabelle_tool2 =
-    Isabelle_Tool("hg_sync", "synchronize Mercurial repository working directory",
+    Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory",
       Scala_Project.here, { args =>
         var clean = false
         var protect: List[String] = Nil
         var root: Option[Path] = None
         var dry_run = false
+        var rev = ""
         var verbose = false
 
         val getopts = Getopts("""
@@ -488,9 +499,10 @@
                  (default: implicit from current directory)
     -f           force changes: no dry-run
     -n           no changes: dry-run
+    -r REV       explicit revision (default: state of working directory)
     -v           verbose
 
-  Synchronize Mercurial repository working directory with other TARGET,
+  Synchronize Mercurial repository with TARGET directory,
   which can be local or remote (using notation of rsync).
 """,
           "C" -> { _ => clean = true; dry_run = true },
@@ -498,6 +510,7 @@
           "R:" -> (arg => root = Some(Path.explode(arg))),
           "f" -> (_ => dry_run = false),
           "n" -> (_ => dry_run = true),
+          "r:" -> (arg => rev = arg),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
@@ -513,9 +526,8 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, verbose = verbose, dry_run = dry_run, clean = clean,
-          filter = protect.map("protect /" + _),
-          progress = progress)
+        hg.sync(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
+          filter = protect.map("protect /" + _), rev = rev)
       }
     )
 }