diff --git a/src/Doc/System/Misc.thy b/src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy
+++ b/src/Doc/System/Misc.thy
@@ -1,452 +1,456 @@
 (*:maxLineLen=78:*)
 
 theory Misc
 imports Base
 begin
 
 chapter \<open>Miscellaneous tools \label{ch:tools}\<close>
 
 text \<open>
   Subsequently we describe various Isabelle related utilities, given in
   alphabetical order.
 \<close>
 
 section \<open>Building Isabelle docker images\<close>
 
 text \<open>
   Docker\<^footnote>\<open>\<^url>\<open>https://docs.docker.com\<close>\<close> provides a self-contained environment
   for complex applications called \<^emph>\<open>container\<close>, although it does not fully
   contain the program in a strict sense of the word. This includes basic
   operating system services (usually based on Linux), shared libraries and
   other required packages. Thus Docker is a light-weight alternative to
   regular virtual machines, or a heavy-weight alternative to conventional
   self-contained applications.
 
   Although Isabelle can be easily run on a variety of OS environments without
   extra containment, Docker images may occasionally be useful when a
   standardized Linux environment is required, even on
   Windows\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-windows\<close>\<close> and
   macOS\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-mac\<close>\<close>. Further uses are in
   common cloud computing environments, where applications need to be submitted
   as Docker images in the first place.
 
   \<^medskip>
   The @{tool_def build_docker} tool builds docker images from a standard
   Isabelle application archive for Linux:
 
   @{verbatim [display]
 \<open>Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
 
   Options are:
     -B NAME      base image (default "ubuntu")
     -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection ("X11", "latex")
     -l NAME      default logic (default ISABELLE_LOGIC="HOL")
     -n           no docker build
     -o FILE      output generated Dockerfile
     -p NAME      additional Ubuntu package
     -t TAG       docker build tag
     -v           verbose
 
   Build Isabelle docker image with default logic image, using a standard
   Isabelle application archive for Linux (local file or remote URL).\<close>}
 
   Option \<^verbatim>\<open>-E\<close> sets \<^verbatim>\<open>bin/isabelle\<close> of the contained Isabelle distribution as
   the standard entry point of the Docker image. Thus \<^verbatim>\<open>docker run\<close> will
   imitate the \<^verbatim>\<open>isabelle\<close> command-line tool (\secref{sec:isabelle-tool}) of a
   regular local installation, but it lacks proper GUI support: \<^verbatim>\<open>isabelle jedit\<close>
   will not work without further provisions. Note that the default entrypoint
   may be changed later via \<^verbatim>\<open>docker run --entrypoint="..."\<close>.
 
   Option \<^verbatim>\<open>-t\<close> specifies the Docker image tag: this a symbolic name within the
   local Docker name space, but also relevant for Docker
   Hub\<^footnote>\<open>\<^url>\<open>https://hub.docker.com\<close>\<close>.
 
   Option \<^verbatim>\<open>-l\<close> specifies the default logic image of the Isabelle distribution
   contained in the Docker environment: it will be produced by \<^verbatim>\<open>isabelle build -b\<close>
   as usual (\secref{sec:tool-build}) and stored within the image.
 
   \<^medskip>
   Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the
   Isabelle installation: it needs to be a suitable version of Ubuntu Linux.
   The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical
   as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For
   Isabelle2021-1 this should be Ubuntu 20.04 LTS.
 
   Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
   of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
 
   Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as
   provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 20.04 LTS). This
   imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will
   only provide remote X11 support according to the modest GUI quality
   standards of the late 1990-ies.
 
   \<^medskip>
   Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close>
   outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a
   Dockerfile only, which might be useful for informative purposes or other
   tools.
 
   Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Produce a Dockerfile (without image) from a remote Isabelle distribution:
   @{verbatim [display]
 \<open>  isabelle build_docker -E -n -o Dockerfile
     https://isabelle.in.tum.de/website-Isabelle2021-1/dist/Isabelle2021-1_linux.tar.gz\<close>}
 
   Build a standard Isabelle Docker image from a local Isabelle distribution,
   with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
 
   @{verbatim [display]
 \<open>  isabelle build_docker -E -t test/isabelle:Isabelle2021-1 Isabelle2021-1_linux.tar.gz\<close>}
 
   Invoke the raw Isabelle/ML process within that image:
   @{verbatim [display]
 \<open>  docker run test/isabelle:Isabelle2021-1 process -e "Session.welcome ()"\<close>}
 
   Invoke a Linux command-line tool within the contained Isabelle system
   environment:
   @{verbatim [display]
 \<open>  docker run test/isabelle:Isabelle2021-1 env uname -a\<close>}
   The latter should always report a Linux operating system, even when running
   on Windows or macOS.
 \<close>
 
 
 section \<open>Managing Isabelle components \label{sec:tool-components}\<close>
 
 text \<open>
   The @{tool_def components} tool manages Isabelle components:
   @{verbatim [display]
 \<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...]
 
   Options are:
     -I           init user settings
     -R URL       component repository (default $ISABELLE_COMPONENT_REPOSITORY)
     -a           resolve all missing components
     -l           list status
     -u DIR       update $ISABELLE_HOME_USER/components: add directory
     -x DIR       update $ISABELLE_HOME_USER/components: remove directory
 
   Resolve Isabelle components via download and installation: given COMPONENTS
   are identified via base name. Further operations manage etc/settings and
   etc/components in $ISABELLE_HOME_USER.
 
   ISABELLE_COMPONENT_REPOSITORY="..."
   ISABELLE_HOME_USER="..."
 \<close>}
 
   Components are initialized as described in \secref{sec:components} in a
   permissive manner, which can mark components as ``missing''. This state is
   amended by letting @{tool "components"} download and unpack components that
   are published on the default component repository
   \<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular.
 
   Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
   \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
 
   Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit
   components may be named as command line-arguments as well. Note that
   components are uniquely identified by their base name, while the
   installation takes place in the location that was specified in the attempt
   to initialize the component before.
 
   \<^medskip>
   Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components
   with their location (full name) within the file-system.
 
   \<^medskip>
   Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
   components specified in the Isabelle repository clone --- this does not make
   any sense for regular Isabelle releases. An existing file that does not
   contain a suitable line ``\<^verbatim>\<open>init_components\<close>\<open>\<dots>\<close>\<^verbatim>\<open>components/main\<close>'' needs
   to be edited according to the printed explanation.
 
   \<^medskip>
   Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in
   \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoids manual editing of
   Isabelle configuration files.
 \<close>
 
 
 section \<open>Viewing documentation \label{sec:tool-doc}\<close>
 
 text \<open>
   The @{tool_def doc} tool displays Isabelle documentation:
   @{verbatim [display]
 \<open>Usage: isabelle doc [DOC ...]
 
   View Isabelle PDF documentation.\<close>}
 
   If called without arguments, it lists all available documents. Each line
   starts with an identifier, followed by a short description. Any of these
   identifiers may be specified as arguments, in order to display the
   corresponding document.
 
   \<^medskip>
   The @{setting ISABELLE_DOCS} setting specifies the list of directories
   (separated by colons) to be scanned for documentations.
 \<close>
 
 
 section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
 
 text \<open>
   The @{tool_def env} tool is a direct wrapper for the standard
   \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle
   settings environment (\secref{sec:settings}).
 
   The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For
   example, the following invokes an instance of the GNU Bash shell within the
   Isabelle environment:
   @{verbatim [display] \<open>isabelle env bash\<close>}
 \<close>
 
 
 section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close>
 
 text \<open>The Isabelle settings environment --- as provided by the
   site-default and user-specific settings files --- can be inspected
   with the @{tool_def getenv} tool:
   @{verbatim [display]
 \<open>Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
 
   Options are:
     -a           display complete environment
     -b           print values only (doesn't work for -a)
     -d FILE      dump complete environment to file (NUL terminated entries)
 
   Get value of VARNAMES from the Isabelle settings.\<close>}
 
   With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that
   Isabelle related programs are run in. This usually contains much more
   variables than are actually Isabelle settings. Normally, output is a list of
   lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values
   to be printed.
 
   Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified
   file. Entries are terminated by the ASCII NUL character, i.e.\ the string
   terminator in C. Thus the Isabelle/Scala operation
   \<^scala_method>\<open>isabelle.Isabelle_System.init\<close> can import the settings
   environment robustly, and provide its own
   \<^scala_method>\<open>isabelle.Isabelle_System.getenv\<close> function.
 \<close>
 
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Get the location of @{setting ISABELLE_HOME_USER} where user-specific
   information is stored:
   @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
 
   \<^medskip>
   Get the value only of the same settings variable, which is particularly
   useful in shell scripts:
   @{verbatim [display] \<open>isabelle getenv -b ISABELLE_HOME_USER\<close>}
 \<close>
 
 
 section \<open>Mercurial repository setup \label{sec:hg-setup}\<close>
 
 text \<open>
   The @{tool_def hg_setup} tool simplifies the setup of Mercurial
   repositories, with hosting via Phabricator (\chref{ch:phabricator}) or SSH
   file server access.
 
   @{verbatim [display]
 \<open>Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
 
   Options are:
     -n NAME      remote repository name (default: base name of LOCAL_DIR)
     -p PATH      Mercurial path name (default: "default")
     -r           assume that remote repository already exists
 
   Setup a remote vs. local Mercurial repository: REMOTE either refers to a
   Phabricator server "user@host" or SSH file server "ssh://user@host/path".\<close>}
 
   The \<^verbatim>\<open>REMOTE\<close> repository specification \<^emph>\<open>excludes\<close> the actual repository
   name: that is given by the base name of \<^verbatim>\<open>LOCAL_DIR\<close>, or via option \<^verbatim>\<open>-n\<close>.
 
   By default, both sides of the repository are created on demand by default.
   In contrast, option \<^verbatim>\<open>-r\<close> assumes that the remote repository already exists:
   it avoids accidental creation of a persistent repository with unintended
   name.
 
   The local \<^verbatim>\<open>.hg/hgrc\<close> file is changed to refer to the remote repository,
   usually via the symbolic path name ``\<^verbatim>\<open>default\<close>''; option \<^verbatim>\<open>-p\<close> allows to
   provide a different name.
 \<close>
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Setup the current directory as a repository with Phabricator server hosting:
   @{verbatim [display] \<open>  isabelle hg_setup vcs@vcs.example.org .\<close>}
 
   \<^medskip>
   Setup the current directory as a repository with plain SSH server hosting:
   @{verbatim [display] \<open>  isabelle hg_setup ssh://files.example.org/data/repositories .\<close>}
 
   \<^medskip>
   Both variants require SSH access to the target server, via public key
   without password.
 \<close>
 
 
 section \<open>Mercurial repository synchronization\<close>
 
 text \<open>
   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
 
   Options are:
     -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
 
   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.
 
   \<^medskip> Option \<^verbatim>\<open>-C\<close> causes deletion of all unknown/ignored files on the target.
   This is potentially dangerous: giving a wrong target directory will cause
   its total destruction! For robustness, option \<^verbatim>\<open>-C\<close> implies option \<^verbatim>\<open>-n\<close>,
   for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
   to force actual deletions on the target.
 
   \<^medskip> Option \<^verbatim>\<open>-P\<close> protects a given file or directory from deletion; multiple
   \<^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 directory, searching upwards until a
   suitable \<^verbatim>\<open>.hg\<close> directory is found.
+
+  \<^medskip> Option \<^verbatim>\<open>-T\<close> indicates a thorough check of file content; the default is to
+  consider files with equal time and size already as equal.
 \<close>
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
   Synchronize the Isabelle repository onto a remote host, while
   protecting a copy of AFP inside of it (without changing that):
   @{verbatim [display] \<open>  isabelle hg_sync -R '$ISABELLE_HOME' -P AFP -C testmachine:test/isabelle\<close>}
 
   So far, this is only a dry run. In a realistic situation, it requires
   consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
 \<close>
 
 
 section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
 
 text \<open>
   By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are
   just run from their location within the distribution directory, probably
   indirectly by the shell through its @{setting PATH}. Other schemes of
   installation are supported by the @{tool_def install} tool:
   @{verbatim [display]
 \<open>Usage: isabelle install [OPTIONS] BINDIR
 
   Options are:
     -d DISTDIR   refer to DISTDIR as Isabelle distribution
                  (default ISABELLE_HOME)
 
   Install Isabelle executables with absolute references to the
   distribution directory.\<close>}
 
   The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as
   determined by @{setting ISABELLE_HOME}.
 
   The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
   @{executable "isabelle"} and @{executable isabelle_scala_script} should be
   placed, which is typically a directory in the shell's @{setting PATH}, such
   as \<^verbatim>\<open>$HOME/bin\<close>.
 
   \<^medskip>
   It is also possible to make symbolic links of the main Isabelle executables
   manually, but making separate copies outside the Isabelle distribution
   directory will not work!
 \<close>
 
 
 section \<open>Creating instances of the Isabelle logo\<close>
 
 text \<open>
   The @{tool_def logo} tool creates variants of the Isabelle logo, for
   inclusion in PDF{\LaTeX} documents.
 
   @{verbatim [display]
 \<open>Usage: isabelle logo [OPTIONS] [NAME]
 
   Options are:
     -o FILE      alternative output file
     -q           quiet mode
 
   Create variant NAME of the Isabelle logo as "isabelle_name.pdf".\<close>}
 
   Option \<^verbatim>\<open>-o\<close> provides an alternative output file, instead of the default in
   the current directory: \<^verbatim>\<open>isabelle_\<close>\<open>name\<close>\<^verbatim>\<open>.pdf\<close> with the lower-case version
   of the given name.
 
   \<^medskip>
   Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name.
 
   \<^medskip>
   Implementors of Isabelle tools and applications are encouraged to make
   derived Isabelle logos for their own projects using this template. The
   license is the same as for the regular Isabelle distribution (BSD).
 \<close>
 
 
 section \<open>Output the version identifier of the Isabelle distribution\<close>
 
 text \<open>
   The @{tool_def version} tool displays Isabelle version information:
   @{verbatim [display]
 \<open>Usage: isabelle version [OPTIONS]
 
   Options are:
     -i           short identification (derived from Mercurial id)
     -t           symbolic tags (derived from Mercurial id)
 
   Display Isabelle version information.\<close>}
 
   \<^medskip>
   The default is to output the full version string of the Isabelle
   distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2021-1: December 2021\<close>.
 
   \<^medskip>
   Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id
   of the @{setting ISABELLE_HOME} directory; option \<^verbatim>\<open>-t\<close> prints version tags
   (if available).
 
   These options require either a repository clone or a repository archive
   (e.g. download of
   \<^url>\<open>https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\<close>).
 \<close>
 
 end
diff --git a/src/Pure/Admin/sync_repos.scala b/src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala
+++ b/src/Pure/Admin/sync_repos.scala
@@ -1,95 +1,100 @@
 /*  Title:      Pure/Admin/sync_repos.scala
     Author:     Makarius
 
 Synchronize Isabelle + AFP repositories.
 */
 
 package isabelle
 
 
 object Sync_Repos {
   def sync_repos(target: String,
     progress: Progress = new Progress,
     verbose: Boolean = false,
+    thorough: Boolean = false,
     dry_run: Boolean = false,
     clean: Boolean = false,
     rev: String = "",
     afp_root: Option[Path] = None,
     afp_rev: String = ""
   ): Unit = {
     val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
 
     val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
     val afp_hg = afp_root.map(Mercurial.repository(_))
 
     def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
-      hg.sync(dest, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
-        rev = r, filter = filter)
+      hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough,
+        dry_run = dry_run, clean = clean, filter = filter)
 
     progress.echo("\n* Isabelle repository:")
     sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect etc/ISABELLE_ID"))
 
     if (!dry_run) {
       Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir =>
         val id_path = tmp_dir + Path.explode("ISABELLE_ID")
         File.write(id_path, isabelle_hg.id(rev = rev))
-        Isabelle_System.rsync(args = List(File.standard_path(id_path), target_dir + "etc/"))
+        Isabelle_System.rsync(thorough = thorough,
+          args = List(File.standard_path(id_path), target_dir + "etc/"))
       }
     }
 
     for (hg <- afp_hg) {
       progress.echo("\n* AFP repository:")
       sync(hg, target_dir + "AFP", afp_rev)
     }
   }
 
   val isabelle_tool =
     Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
       Scala_Project.here, { args =>
         var afp_root: Option[Path] = None
         var clean = false
+        var thorough = false
         var afp_rev = ""
         var dry_run = false
         var rev = ""
         var verbose = false
 
         val getopts = Getopts("""
 Usage: isabelle sync_repos [OPTIONS] TARGET
 
   Options are:
     -A ROOT      include AFP with given root directory
     -C           clean all unknown/ignored files on target
                  (implies -n for testing; use option -f to confirm)
+    -T           thorough check of file content (default: time and size)
     -a REV       explicit AFP revision (default: state of working directory)
     -f           force changes: no dry-run
     -n           no changes: dry-run
     -r REV       explicit revision (default: state of working directory)
     -v           verbose
 
   Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
 
   Example (without -f as "dry-run"):
 
     isabelle sync_repos -A '$AFP_BASE' -C testmachine:test/isabelle_afp
 """,
           "A:" -> (arg => afp_root = Some(Path.explode(arg))),
           "C" -> { _ => clean = true; dry_run = true },
+          "T" -> (_ => thorough = true),
           "a:" -> (arg => afp_rev = arg),
           "f" -> (_ => dry_run = false),
           "n" -> (_ => dry_run = true),
           "r:" -> (arg => rev = arg),
           "v" -> (_ => verbose = true))
 
         val more_args = getopts(args)
         val target =
           more_args match {
             case List(target) => target
             case _ => getopts.usage()
           }
 
         val progress = new Console_Progress
-        sync_repos(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
-          rev = rev, afp_root = afp_root, afp_rev = afp_rev)
+        sync_repos(target, progress = progress, verbose = verbose, thorough = thorough,
+          dry_run = dry_run, clean = clean, rev = rev, afp_root = afp_root, afp_rev = afp_rev)
       }
     )
 }
diff --git a/src/Pure/General/mercurial.scala b/src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala
+++ b/src/Pure/General/mercurial.scala
@@ -1,535 +1,541 @@
 /*  Title:      Pure/General/mercurial.scala
     Author:     Makarius
 
 Support for Mercurial repositories, with local or remote repository clone
 and working directory (via ssh connection).
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 
 
 object Mercurial {
   type Graph = isabelle.Graph[String, Unit]
 
 
 
   /** HTTP server **/
 
   object Server {
     def apply(root: String): Server = new Server(root)
 
     def start(root: Path): Server = {
       val hg = repository(root)
 
       val server_process = Future.promise[Bash.Process]
       val server_root = Future.promise[String]
       Isabelle_Thread.fork("hg") {
         val process =
           Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
         server_process.fulfill_result(process)
         Exn.release(process).result(progress_stdout =
           line => if (!server_root.is_finished) {
             server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line))
           })
       }
       server_process.join
 
       new Server(server_root.join) {
         override def close(): Unit = server_process.join.terminate()
       }
     }
   }
 
   class Server private(val root: String) extends AutoCloseable {
     override def toString: String = root
 
     def close(): Unit = ()
 
     def changeset(rev: String = "tip", raw: Boolean = false): String =
       root + (if (raw) "/raw-rev/" else "/rev/") + rev
 
     def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
       root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode
 
     def archive(rev: String = "tip"): String =
       root + "/archive/" + rev + ".tar.gz"
 
     def read_changeset(rev: String = "tip"): String =
       Url.read(changeset(rev = rev, raw = true))
 
     def read_file(path: Path, rev: String = "tip"): String =
       Url.read(file(path, rev = rev, raw = true))
 
     def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content =
       Isabelle_System.download(archive(rev = rev), progress = progress)
 
     def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit = {
       Isabelle_System.new_directory(dir)
       Isabelle_System.with_tmp_file("rev", ext = ".tar.gz") { archive_path =>
         val content = download_archive(rev = rev, progress = progress)
         Bytes.write(archive_path, content.bytes)
         progress.echo("Unpacking " + rev + ".tar.gz")
         Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
           dir = dir, original_owner = true, strip = 1).check
       }
     }
   }
 
 
 
   /** repository commands **/
 
   /* command-line syntax */
 
   def optional(s: String, prefix: String = ""): String =
     if (s == "") "" else " " + prefix + " " + Bash.string(s)
 
   def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
   def opt_rev(s: String): String = optional(s, "--rev")
   def opt_template(s: String): String = optional(s, "--template")
 
 
   /* repository archives */
 
   private val Archive_Node = """^node: (\S{12}).*$""".r
   private val Archive_Tag = """^tag: (\S+).*$""".r
 
   sealed case class Archive_Info(lines: List[String]) {
     def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
     def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
   }
 
   def archive_info(root: Path): Option[Archive_Info] = {
     val path = root + Path.explode(".hg_archival.txt")
     if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None
   }
 
   def archive_id(root: Path): Option[String] =
     archive_info(root).flatMap(_.id)
 
   def archive_tags(root: Path): Option[String] =
     archive_info(root).map(info => info.tags.mkString(" "))
 
 
   /* repository access */
 
   def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
     ssh.is_dir(root + Path.explode(".hg")) &&
     new Repository(root, ssh).command("root").ok
 
   def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = {
     val hg = new Repository(root, ssh)
     hg.command("root").check
     hg
   }
 
   def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = {
     @tailrec def find(root: Path): Option[Repository] =
       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
       else if (root.is_root) None
       else find(root + Path.parent)
 
     find(ssh.expand_path(start))
   }
 
   def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository =
     find_repository(start, ssh = ssh) getOrElse
       error("No repository found in " + start.absolute)
 
   private def make_repository(
     root: Path,
     cmd: String,
     args: String,
     ssh: SSH.System = SSH.Local
   ) : Repository = {
     val hg = new Repository(root, ssh)
     ssh.make_directory(hg.root.dir)
     hg.command(cmd, args, repository = false).check
     hg
   }
 
   def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
     make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
 
   def clone_repository(source: String, root: Path,
       rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
     make_repository(root, "clone",
       options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
 
   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository = {
     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   }
 
   class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local) {
     hg =>
 
     val root: Path = ssh.expand_path(root_path)
     def root_url: String = ssh.hg_url + root.implode
 
     override def toString: String = ssh.hg_url + root.implode
 
     def command_line(
       name: String,
       args: String = "",
       options: String = "",
       repository: Boolean = true
     ): String = {
       "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
         (if (repository) " --repository " + ssh.bash_path(root) else "") +
         " --noninteractive " + name + " " + options + " " + args
     }
 
     def command(
       name: String,
       args: String = "",
       options: String = "",
       repository: Boolean = true
     ): Process_Result = {
       ssh.execute(command_line(name, args = args, options = options, repository = repository))
     }
 
     def add(files: List[Path]): Unit =
       hg.command("add", files.map(ssh.bash_path).mkString(" "))
 
     def archive(target: String, rev: String = "", options: String = ""): Unit =
       hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
 
     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
       hg.command("heads", opt_template(template), options).check.out_lines
 
     def identify(rev: String = "tip", options: String = ""): String =
       hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
 
     def id(rev: String = "tip"): String = identify(rev, options = "-i")
 
     def tags(rev: String = "tip"): String = {
       val result = identify(rev, options = "-t")
       Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
     }
 
     def paths(args: String = "", options: String = ""): List[String] =
       hg.command("paths", args = args, options = options).check.out_lines
 
     def manifest(rev: String = "", options: String = ""): List[String] =
       hg.command("manifest", opt_rev(rev), options).check.out_lines
 
     def log(rev: String = "", template: String = "", options: String = ""): String =
       hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
 
     def parent(): String = log(rev = "p1()", template = "{node|short}")
 
     def push(
       remote: String = "",
       rev: String = "",
       force: Boolean = false,
       options: String = ""
     ): Unit = {
       hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
         check_rc(rc => rc == 0 | rc == 1)
     }
 
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
       hg.command("pull", opt_rev(rev) + optional(remote), options).check
 
     def update(
       rev: String = "",
       clean: Boolean = false,
       check: Boolean = false,
       options: String = ""
     ): Unit = {
       hg.command("update",
         opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
     }
 
     def status(options: String = ""): List[String] =
       hg.command("status", options = options).check.out_lines
 
     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 = {
       require(ssh == SSH.Local, "local repository required")
 
       Isabelle_System.with_tmp_dir("rsync") { tmp_dir =>
         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 = File.standard_path(root)
             (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,
+          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 = {
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
       val log_result =
         log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
       split_lines(log_result).foldLeft(Graph.string[Unit]) {
         case (graph, Node(x, y, z)) =>
           val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
           val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ()))
           deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) })
         case (graph, _) => graph
       }
     }
   }
 
 
 
   /** check files **/
 
   def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) = {
     val outside = new mutable.ListBuffer[Path]
     val unknown = new mutable.ListBuffer[Path]
 
     @tailrec def check(paths: List[Path]): Unit = {
       paths match {
         case path :: rest =>
           find_repository(path, ssh) match {
             case None => outside += path; check(rest)
             case Some(hg) =>
               val known =
                 hg.known_files().iterator.map(name =>
                   (hg.root + Path.explode(name)).canonical_file).toSet
               if (!known(path.canonical_file)) unknown += path
               check(rest.filterNot(p => known(p.canonical_file)))
           }
         case Nil =>
       }
     }
 
     check(files)
     (outside.toList, unknown.toList)
   }
 
 
 
   /** hg_setup **/
 
   private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit = {
     val hgrc = local_hg.root + Path.explode(".hg/hgrc")
     def header(line: String): Boolean = line.startsWith("[paths]")
     val Entry = """^(\S+)\s*=\s*(.*)$""".r
     val new_entry = path_name + " = " + source
 
     def commit(lines: List[String]): Boolean = {
       File.write(hgrc, cat_lines(lines))
       true
     }
     val edited =
       hgrc.is_file && {
         val lines = split_lines(File.read(hgrc))
         lines.count(header) == 1 && {
           if (local_hg.paths(options = "-q").contains(path_name)) {
             val old_source = local_hg.paths(args = path_name).head
             val old_entry = path_name + ".old = " + old_source
             val lines1 =
               lines.map {
                 case Entry(a, b) if a == path_name && b == old_source =>
                   new_entry + "\n" + old_entry
                 case line => line
               }
             lines != lines1 && commit(lines1)
           }
           else {
             val prefix = lines.takeWhile(line => !header(line))
             val n = prefix.length
             commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1))
           }
         }
       }
     if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n")
   }
 
   val default_path_name = "default"
 
   def hg_setup(
     remote: String,
     local_path: Path,
     remote_name: String = "",
     path_name: String = default_path_name,
     remote_exists: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
     /* local repository */
 
     Isabelle_System.make_directory(local_path)
 
     val repos_name =
       proper_string(remote_name) getOrElse local_path.absolute.base.implode
 
     val local_hg =
       if (is_repository(local_path)) repository(local_path)
       else init_repository(local_path)
 
     progress.echo("Local repository " + local_hg.root.absolute)
 
 
     /* remote repository */
 
     val remote_url =
       remote match {
         case _ if remote.startsWith("ssh://") =>
           val ssh_url = remote + "/" + repos_name
 
           if (!remote_exists) {
             try { local_hg.command("init", ssh_url, repository = false).check }
             catch { case ERROR(msg) => progress.echo_warning(msg) }
           }
 
           ssh_url
 
         case SSH.Target(user, host) =>
           val phabricator = Phabricator.API(user, host)
 
           var repos =
             phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
               if (remote_exists) {
                 error("Remote repository " +
                   quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
               }
               else phabricator.create_repository(repos_name, short_name = repos_name)
             }
 
           while (repos.importing) {
             progress.echo("Awaiting remote repository ...")
             Time.seconds(0.5).sleep()
             repos = phabricator.the_repository(repos.phid)
           }
 
           repos.ssh_url
 
         case _ => error("Malformed remote specification " + quote(remote))
       }
 
     progress.echo("Remote repository " + quote(remote_url))
 
 
     /* synchronize local and remote state */
 
     progress.echo("Synchronizing ...")
 
     edit_hgrc(local_hg, path_name, remote_url)
 
     local_hg.pull(options = "-u")
 
     local_hg.push(remote = remote_url)
   }
 
   val isabelle_tool1 =
     Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
       Scala_Project.here,
       { args =>
         var remote_name = ""
         var path_name = default_path_name
         var remote_exists = false
 
         val getopts = Getopts("""
 Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
 
   Options are:
     -n NAME      remote repository name (default: base name of LOCAL_DIR)
     -p PATH      Mercurial path name (default: """ + quote(default_path_name) + """)
     -r           assume that remote repository already exists
 
   Setup a remote vs. local Mercurial repository: REMOTE either refers to a
   Phabricator server "user@host" or SSH file server "ssh://user@host/path".
 """,
           "n:" -> (arg => remote_name = arg),
           "p:" -> (arg => path_name = arg),
           "r" -> (_ => remote_exists = true))
 
         val more_args = getopts(args)
 
         val (remote, local_path) =
           more_args match {
             case List(arg1, arg2) => (arg1, Path.explode(arg2))
             case _ => getopts.usage()
           }
 
         val progress = new Console_Progress
 
         hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
           remote_exists = remote_exists, progress = progress)
       })
 
 
 
   /** hg_sync **/
 
   val isabelle_tool2 =
     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("""
 Usage: isabelle hg_sync [OPTIONS] TARGET
 
   Options are:
     -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
 
   Synchronize Mercurial repository with TARGET directory,
   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 more_args = getopts(args)
         val target =
           more_args match {
             case List(target) => target
             case _ => getopts.usage()
           }
 
         val progress = new Console_Progress
         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 /" + _))
       }
     )
 }
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,521 +1,523 @@
 /*  Title:      Pure/System/isabelle_system.scala
     Author:     Makarius
 
 Miscellaneous Isabelle system operations.
 */
 
 package isabelle
 
 
 import java.util.{Map => JMap, HashMap}
 import java.io.{File => JFile, IOException}
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
   StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 
 import scala.jdk.CollectionConverters._
 
 
 object Isabelle_System {
   /* settings environment */
 
   def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = {
     val env0 = isabelle.setup.Environment.settings()
     if (putenv.isEmpty) env0
     else {
       val env = new HashMap(env0)
       for ((a, b) <- putenv) env.put(a, b)
       env
     }
   }
 
   def getenv(name: String, env: JMap[String, String] = settings()): String =
     Option(env.get(name)).getOrElse("")
 
   def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))
 
 
   /* services */
 
   abstract class Service
 
   @volatile private var _services: Option[List[Class[Service]]] = None
 
   def services(): List[Class[Service]] = {
     if (_services.isEmpty) init()  // unsynchronized check
     _services.get
   }
 
   def make_services[C](c: Class[C]): List[C] =
     for { c1 <- services() if Library.is_subclass(c1, c) }
       yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
 
 
   /* init settings + services */
 
   def make_services(): List[Class[Service]] = {
     def make(where: String, names: List[String]): List[Class[Service]] = {
       for (name <- names) yield {
         def err(msg: String): Nothing =
           error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
         try { Class.forName(name).asInstanceOf[Class[Service]] }
         catch {
           case _: ClassNotFoundException => err("Class not found")
           case exn: Throwable => err(Exn.message(exn))
         }
       }
     }
 
     def from_env(variable: String): List[Class[Service]] =
       make(quote(variable), space_explode(':', getenv_strict(variable)))
 
     def from_jar(platform_jar: String): List[Class[Service]] =
       make(quote(platform_jar),
         isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList)
 
     from_env("ISABELLE_SCALA_SERVICES") ::: Scala.class_path().flatMap(from_jar)
   }
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = {
     isabelle.setup.Environment.init(isabelle_root, cygwin_root)
     synchronized { if (_services.isEmpty) { _services = Some(make_services()) } }
   }
 
 
   /* getetc -- static distribution parameters */
 
   def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = {
     val path = root + Path.basic("etc") + Path.basic(name)
     if (path.is_file) {
       Library.trim_split_lines(File.read(path)) match {
         case Nil => None
         case List(s) => Some(s)
         case _ => error("Single line expected in " + path.absolute)
       }
     }
     else None
   }
 
 
   /* Isabelle distribution identification */
 
   def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
       if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
       else error("Failed to identify Isabelle distribution " + root.expand)
     }
 
   object Isabelle_Id extends Scala.Fun_String("isabelle_id") {
     val here = Scala_Project.here
     def apply(arg: String): String = isabelle_id()
   }
 
   def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
       if (Mercurial.is_repository(root)) {
         val hg = Mercurial.repository(root)
         hg.tags(rev = hg.parent())
       }
       else ""
     }
 
   def export_isabelle_identifier(isabelle_identifier: String): String =
     if (isabelle_identifier == "") ""
     else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
 
   def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
 
   def isabelle_heading(): String =
     isabelle_identifier() match {
       case None => ""
       case Some(version) => " (" + version + ")"
     }
 
   def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
 
   def identification(): String =
     "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading()
 
 
   /** file-system operations **/
 
   /* scala functions */
 
   private def apply_paths(
     args: List[String],
     fun: PartialFunction[List[Path], Unit]
   ): List[String] = {
     fun(args.map(Path.explode))
     Nil
   }
 
   private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
     apply_paths(args, { case List(path) => fun(path) })
 
   private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
     apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
 
   private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
     apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
 
   def chmod(arg: String, path: Path): Unit =
     bash("chmod " + arg + " " + File.bash_path(path)).check
 
   def chown(arg: String, path: Path): Unit =
     bash("chown " + arg + " " + File.bash_path(path)).check
 
 
   /* directories */
 
   def make_directory(path: Path): Path = {
     if (!path.is_dir) {
       try { Files.createDirectories(path.java_path) }
       catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
     }
     path
   }
 
   def new_directory(path: Path): Path =
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)
 
   def copy_dir(dir1: Path, dir2: Path): Unit = {
     val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
     if (!res.ok) {
       cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
     }
   }
 
   def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = {
     if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute)
     else {
       try { copy_dir(dir1, dir2); body }
       finally { rm_tree(dir2 ) }
     }
   }
 
 
   object Make_Directory extends Scala.Fun_Strings("make_directory") {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
   }
 
   object Copy_Dir extends Scala.Fun_Strings("copy_dir") {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
   }
 
 
   /* copy files */
 
   def copy_file(src: JFile, dst: JFile): Unit = {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target)) {
       try {
         Files.copy(src.toPath, target.toPath,
           StandardCopyOption.COPY_ATTRIBUTES,
           StandardCopyOption.REPLACE_EXISTING)
       }
       catch {
         case ERROR(msg) =>
           cat_error("Failed to copy file " +
             File.path(src).absolute + " to " + File.path(dst).absolute, msg)
       }
     }
   }
 
   def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
 
   def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
     val src1 = src.expand
     val src1_dir = src1.dir
     if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
     copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
   }
 
 
   object Copy_File extends Scala.Fun_Strings("copy_file") {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
   }
 
   object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
   }
 
 
   /* move files */
 
   def move_file(src: JFile, dst: JFile): Unit = {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target))
       Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
   }
 
   def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
 
 
   /* symbolic link */
 
   def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = {
     val src_file = src.file
     val dst_file = dst.file
     val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
 
     if (force) target.delete
 
     def cygwin_link(): Unit = {
       if (native) {
         error("Failed to create native symlink on Windows: " + quote(src_file.toString) +
           "\n(but it could work as Administrator)")
       }
       else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
     }
 
 
     try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
     catch {
       case _: UnsupportedOperationException if Platform.is_windows => cygwin_link()
       case _: FileSystemException if Platform.is_windows => cygwin_link()
     }
   }
 
 
   /* tmp files */
 
   def isabelle_tmp_prefix(): JFile = {
     val path = Path.explode("$ISABELLE_TMP_PREFIX")
     path.file.mkdirs  // low-level mkdirs to avoid recursion via Isabelle environment
     File.platform_file(path)
   }
 
   def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = {
     val suffix = if (ext == "") "" else "." + ext
     val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
     file.deleteOnExit()
     file
   }
 
   def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = {
     val file = tmp_file(name, ext)
     try { body(File.path(file)) } finally { file.delete }
   }
 
 
   /* tmp dirs */
 
   def rm_tree(root: JFile): Unit = {
     root.delete
     if (root.isDirectory) {
       Files.walkFileTree(root.toPath,
         new SimpleFileVisitor[JPath] {
           override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = {
             try { Files.deleteIfExists(file) }
             catch { case _: IOException => }
             FileVisitResult.CONTINUE
           }
 
           override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = {
             if (e == null) {
               try { Files.deleteIfExists(dir) }
               catch { case _: IOException => }
               FileVisitResult.CONTINUE
             }
             else throw e
           }
         }
       )
     }
   }
 
   def rm_tree(root: Path): Unit = rm_tree(root.file)
 
   object Rm_Tree extends Scala.Fun_Strings("rm_tree") {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
   }
 
   def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = {
     val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
     dir.deleteOnExit()
     dir
   }
 
   def with_tmp_dir[A](name: String)(body: Path => A): A = {
     val dir = tmp_dir(name)
     try { body(File.path(dir)) } finally { rm_tree(dir) }
   }
 
 
   /* quasi-atomic update of directory */
 
   def update_directory(dir: Path, f: Path => Unit): Unit = {
     val new_dir = dir.ext("new")
     val old_dir = dir.ext("old")
 
     rm_tree(new_dir)
     rm_tree(old_dir)
 
     f(new_dir)
 
     if (dir.is_dir) move_file(dir, old_dir)
     move_file(new_dir, dir)
     rm_tree(old_dir)
   }
 
 
 
   /** external processes **/
 
   /* GNU bash */
 
   def bash(script: String,
     description: String = "",
     cwd: JFile = null,
     env: JMap[String, String] = settings(),
     redirect: Boolean = false,
     input: String = "",
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
     watchdog: Option[Bash.Watchdog] = None,
     strict: Boolean = true,
     cleanup: () => Unit = () => ()
   ): Process_Result = {
     Bash.process(script,
       description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
       result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr,
         watchdog = watchdog, strict = strict)
   }
 
 
   /* command-line tools */
 
   def require_command(cmd: String, test: String = "--version"): Unit = {
     if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd))
   }
 
   private lazy val gnutar_check: Boolean =
     try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
     catch { case ERROR(_) => false }
 
   def gnutar(
     args: String,
     dir: Path = Path.current,
     original_owner: Boolean = false,
     strip: Int = 0,
     redirect: Boolean = false
   ): Process_Result = {
     val options =
       (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
       (if (original_owner) "" else "--owner=root --group=staff ") +
       (if (strip <= 0) "" else "--strip-components=" + strip + " ")
 
     if (gnutar_check) bash("tar " + options + args, redirect = redirect)
     else error("Expected to find GNU tar executable")
   }
 
   def rsync(
     cwd: JFile = null,
     progress: Progress = new Progress,
     verbose: Boolean = false,
+    thorough: Boolean = false,
     dry_run: Boolean = false,
     clean: Boolean = false,
     filter: List[String] = Nil,
     args: List[String] = Nil
   ): Unit = {
     val script =
       "rsync --protect-args --archive" +
         (if (verbose || dry_run) " --verbose" else "") +
+        (if (thorough) " --ignore-times" else "") +
         (if (dry_run) " --dry-run" else "") +
         (if (clean) " --delete-excluded" else "") +
         filter.map(s => " --filter=" + Bash.string(s)).mkString +
         (if (args.nonEmpty) " " + Bash.strings(args) else "")
     progress.bash(script, cwd = cwd, echo = true).check
   }
 
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
     with_tmp_file("patch") { patch =>
       Isabelle_System.bash(
         "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) +
           " > " + File.bash_path(patch),
         cwd = base_dir.file).check_rc(_ <= 1)
       File.read(patch)
     }
   }
 
   def hostname(): String = bash("hostname -s").check.out
 
   def open(arg: String): Unit =
     bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
 
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
   def open_external_file(name: String): Boolean = {
     val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
     val external =
       ext.nonEmpty &&
       Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
     if (external) {
       if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
       else open(name)
     }
     external
   }
 
 
 
   /** Isabelle resources **/
 
   /* repository clone with Admin */
 
   def admin(): Boolean = Path.explode("~~/Admin").is_dir
 
 
   /* default logic */
 
   def default_logic(args: String*): String = {
     args.find(_ != "") match {
       case Some(logic) => logic
       case None => getenv_strict("ISABELLE_LOGIC")
     }
   }
 
 
   /* download file */
 
   def download(url_name: String, progress: Progress = new Progress): HTTP.Content = {
     val url = Url(url_name)
     progress.echo("Getting " + quote(url_name))
     try { HTTP.Client.get(url) }
     catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
   }
 
   def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
     Bytes.write(file, download(url_name, progress = progress).bytes)
 
   object Download extends Scala.Fun("download", thread = true) {
     val here = Scala_Project.here
     override def invoke(args: List[Bytes]): List[Bytes] =
       args.map(url => download(url.text).bytes)
   }
 
 
   /* repositories */
 
   val isabelle_repository: Mercurial.Server =
     Mercurial.Server("https://isabelle.sketis.net/repos/isabelle")
 
   val afp_repository: Mercurial.Server =
     Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel")
 
   def official_releases(): List[String] =
     Library.trim_split_lines(
       isabelle_repository.read_file(Path.explode("Admin/Release/official")))
 }