# HG changeset patch
# User wenzelm
# Date 1655112719 -7200
# Node ID df14a62129e92394aad5e1f592a2c5c90edb88bf
# Parent  1f6fc2416a482708e93cb0a423aaac8452199c8e
misc tuning;

diff -r 1f6fc2416a48 -r df14a62129e9 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Jun 13 11:10:39 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Jun 13 11:31:59 2022 +0200
@@ -865,10 +865,9 @@
 section \<open>Synchronize source repositories and session images for Isabelle and AFP\<close>
 
 text \<open>
-  The @{tool_def sync} tool synchronizes a local Isabelle and AFP repository
-  clone, potentially including its prebuilt \<^verbatim>\<open>.jar\<close> files and session images.
-
-  @{verbatim [display]
+  The @{tool_def sync} tool synchronizes a local Isabelle and AFP source
+  repository, possibly with prebuilt \<^verbatim>\<open>.jar\<close> files and session images. Its
+  command-line usage is: @{verbatim [display]
 \<open>Usage: isabelle sync [OPTIONS] TARGET
 
   Options are:
@@ -888,9 +887,9 @@
 
   Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".\<close>}
 
-  The approach is to apply @{tool hg_sync} (\secref{sec:tool-hg-sync}) on the
-  underlying Isabelle repository plus a given AFP repository (optional). This
-  means that the Isabelle installation needs to be a Mercurial repository
+  The approach is to apply @{tool hg_sync} (see \secref{sec:tool-hg-sync}) on
+  the underlying Isabelle repository, and an optional AFP repository.
+  Consequently, the Isabelle installation needs to be a Mercurial repository
   clone: a regular download of the Isabelle distribution is not sufficient!
 
   On the target side, AFP is placed into @{setting ISABELLE_HOME} as immediate
@@ -904,55 +903,59 @@
   but for the Isabelle and AFP repositories, respectively. The AFP version is
   only used if a corresponding repository is given via option \<^verbatim>\<open>-A\<close>, either
   with explicit root directory, or as \<^verbatim>\<open>-A:\<close> to refer to \<^verbatim>\<open>$AFP_BASE\<close> (this
-  assumes AFP as component of the local Isabelle installation).
+  assumes AFP as component of the local Isabelle installation). If no AFP
+  repository is given, an existing \<^verbatim>\<open>AFP\<close> directory on the target remains
+  unchanged.
 
-  \<^medskip> Option \<^verbatim>\<open>-J\<close> uploads existing \<^verbatim>\<open>.jar\<close> files, which are usually
-  Isabelle/Scala/Java modules under control of \<^verbatim>\<open>etc/build.props\<close> (see also
-  \secref{sec:scala-build}). Normally, the underlying dependency management is
-  accurate: bad uploads will be rebuilt on the remote side (or ignored). For
-  historic Isabelle versions, going far back into the past via option \<^verbatim>\<open>-r\<close>,
-  it is better to omit option \<^verbatim>\<open>-J\<close> and thus purge \<^verbatim>\<open>.jar\<close> files on the target
-  (because they do not belong to the repository).
+  \<^medskip> Option \<^verbatim>\<open>-J\<close> uploads existing \<^verbatim>\<open>.jar\<close> files from the working directory,
+  which are usually Isabelle/Scala/Java modules under control of @{tool
+  scala_build} via \<^verbatim>\<open>etc/build.props\<close> (see also \secref{sec:scala-build}).
+  Thus the dependency management is accurate: bad uploads will be rebuilt
+  eventually (or ignored). This might fail for very old Isabelle versions,
+  when going into the past via option \<^verbatim>\<open>-r\<close>: here it is better to omit option
+  \<^verbatim>\<open>-J\<close> and thus purge \<^verbatim>\<open>.jar\<close> files on the target (because they do not belong
+  to the repository).
 
   \<^medskip> Option \<^verbatim>\<open>-I\<close> uploads a collection of session images. The set of \<^verbatim>\<open>-I\<close>
   options specifies the end-points in the session build graph, including all
   required ancestors. The result collection is uploaded using the underlying
-  \<^verbatim>\<open>rsync\<close> policies: unchanged images are ignored. Session images are
-  assembled within the target \<^verbatim>\<open>heaps\<close> directory: this scheme fits together
-  with @{tool build}~\<^verbatim>\<open>-o system_heaps\<close>. Images are taken as-is from the local
-  Isabelle installation, regardless of option \<^verbatim>\<open>-r\<close>. Bad images do not cause
-  any harm, apart from wasting network bandwidth and file-system space:
-  running e.g. @{tool build} on the target will check dependencies accurately,
-  and rebuild outdated images on demand.
+  \<^verbatim>\<open>rsync\<close> policies, so unchanged images are not sent again. Session images
+  are assembled within the target \<^verbatim>\<open>heaps\<close> directory: this scheme fits
+  together with @{tool build}~\<^verbatim>\<open>-o system_heaps\<close>. Images are taken as-is from
+  the local Isabelle installation, regardless of option \<^verbatim>\<open>-r\<close>. Upload of bad
+  images could waste time and space, but running e.g. @{tool build} on the
+  target will check dependencies accurately and rebuild outdated images on
+  demand.
 
   \<^medskip> Option \<^verbatim>\<open>-H\<close> tells the underlying \<^verbatim>\<open>rsync\<close> process to purge the \<^verbatim>\<open>heaps\<close>
-  directory on the target, before uploading new images from \<^verbatim>\<open>-I\<close> options. The
+  directory on the target, before uploading new images via option \<^verbatim>\<open>-I\<close>. The
   default is to work monotonically: old material that is not overwritten
-  remains unchanged, it is never deleted. Over time, this may lead to
-  unreachable garbage, due to changes in session names or Poly/ML versions.
-  Option \<^verbatim>\<open>-H\<close> helps to avoid wasting file-system space, although @{tool
-  build} does not require it, due to its precise checking of all dependencies.
+  remains unchanged. Over time, this may lead to unused garbage, due to
+  changes in session names or the Poly/ML version. Option \<^verbatim>\<open>-H\<close> helps to avoid
+  wasting file-system space.
 
   \<^medskip> Option \<^verbatim>\<open>-S\<close> uses \<^verbatim>\<open>rsync --protect-args\<close>, but this requires at least
-  \<^verbatim>\<open>rsync 3.0.0\<close>, while many versions of macOS still ship \<^verbatim>\<open>rsync 2.9.x\<close>.
-  Since Isabelle + AFP don't use spaces or other special characters, it is
-  usually safe to omit this non-portable option.
+  \<^verbatim>\<open>rsync 3.0.0\<close>, while macOS might only provide \<^verbatim>\<open>rsync 2.9.x\<close>. Since
+  Isabelle + AFP don't use spaces or other special characters, it is usually
+  safe to omit this non-portable option.
 \<close>
 
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Quick testing of Isabelle + AFP on a remote machine: upload changed sources,
-  jars, and local sessions images for \<^verbatim>\<open>HOL\<close>:
+  For quick testing of Isabelle + AFP on a remote machine, upload changed
+  sources, jars, and local sessions images for \<^verbatim>\<open>HOL\<close>:
+
   @{verbatim [display] \<open>  isabelle sync -A: -I HOL -J testmachine:test/isabelle_afp\<close>}
   Assuming that the local \<^verbatim>\<open>HOL\<close> hierarchy has been up-to-date, and the local
   and remote ML platforms coincide, a remote @{tool build} will proceed
   without building \<^verbatim>\<open>HOL\<close> again.
 
-  \<^medskip> A variation for accurate testing of Isabelle + AFP: no option \<^verbatim>\<open>-J\<close>, but
-  option \<^verbatim>\<open>-T\<close> to disable the default ``quick check'' of \<^verbatim>\<open>rsync\<close> (which only
-  inspects file sizes and date stamps):
-  @{verbatim [display] \<open> isabelle sync -A: -T testmachine:test/isabelle_afp\<close>}
+  \<^medskip> Here is a variation for extra-clean testing of Isabelle + AFP: no option
+  \<^verbatim>\<open>-J\<close>, but option \<^verbatim>\<open>-T\<close> to disable the default ``quick check'' of \<^verbatim>\<open>rsync\<close>
+  (which only inspects file sizes and date stamps); existing heaps are
+  deleted:
+  @{verbatim [display] \<open> isabelle sync -A: -T -H testmachine:test/isabelle_afp\<close>}
 \<close>
 
 end