src/Pure/General/mercurial.scala

     def known_files(): List[String] = status(options = "--modified --added --clean --no-status")
 
     def sync(target: String,
       progress: Progress = new Progress,
       verbose: Boolean = false,
+      thorough: Boolean = false,
       dry_run: Boolean = false,
       clean: Boolean = false,
       filter: List[String] = Nil,
       rev: String = ""
     ): Unit = {

             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,
+          progress = progress, verbose = verbose, thorough = thorough,
+          dry_run = dry_run, clean = clean, filter = filter,
           args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target))
       }
     }
 
     def graph(): Graph = {

     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 thorough = false
         var dry_run = false
         var rev = ""
         var verbose = false
 
         val getopts = Getopts("""

     -C           clean all unknown/ignored files on target
                  (implies -n for testing; use option -f to confirm)
     -P NAME      protect NAME within TARGET from deletion
     -R ROOT      explicit repository root directory
                  (default: implicit from current directory)
+    -T           thorough check of file content (default: time and size)
     -f           force changes: no dry-run
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
     -v           verbose
 

   which can be local or remote (using notation of rsync).
 """,
           "C" -> { _ => clean = true; dry_run = true },
           "P:" -> (arg => protect = protect ::: List(arg)),
           "R:" -> (arg => root = Some(Path.explode(arg))),
+          "T" -> (_ => thorough = true),
           "f" -> (_ => dry_run = false),
           "n" -> (_ => dry_run = true),
           "r:" -> (arg => rev = arg),
           "v" -> (_ => verbose = true))
 

         val hg =
           root match {
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
-          filter = protect.map("protect /" + _), rev = rev)
+        hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
+          dry_run = dry_run, clean = clean, rev = rev,
+          filter = protect.map("protect /" + _))
       }
     )
 }