diff -r 4aa3da02fd4d -r 4dd0f250ec0d src/Pure/Admin/sync.scala --- a/src/Pure/Admin/sync.scala Fri Jun 10 21:05:31 2022 +0200 +++ b/src/Pure/Admin/sync.scala Fri Jun 10 23:53:09 2022 +0200 @@ -36,6 +36,7 @@ def sync(options: Options, context: Rsync.Context, target: String, verbose: Boolean = false, thorough: Boolean = false, + purge_heaps: Boolean = false, session_images: List[String] = Nil, preserve_jars: Boolean = false, dry_run: Boolean = false, @@ -56,9 +57,10 @@ } context.progress.echo_if(verbose, "\n* Isabelle repository:") + val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**") sync(hg, target, rev, contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))), - filter = List("protect /heaps", "protect /heaps/**", "protect /AFP")) + filter = filter_heaps ::: List("protect /AFP")) for (hg <- afp_hg) { context.progress.echo_if(verbose, "\n* AFP repository:") @@ -79,6 +81,7 @@ Isabelle_Tool("sync", "synchronize Isabelle + AFP repositories", Scala_Project.here, { args => var afp_root: Option[Path] = None + var purge_heaps = false var session_images = List.empty[String] var preserve_jars = false var protect_args = false @@ -94,6 +97,7 @@ Options are: -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) + -H purge heaps directory on target -I NAME include session heap image and build database (based on accidental local state) -J preserve *.jar files @@ -120,6 +124,7 @@ isabelle sync -A: -I HOL-Analysis testmachine:test/isabelle_afp """, "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), + "H" -> (_ => purge_heaps = true), "I:" -> (arg => session_images = session_images ::: List(arg)), "J" -> (_ => preserve_jars = true), "S" -> (_ => protect_args = true), @@ -141,9 +146,8 @@ val progress = new Console_Progress val context = Rsync.Context(progress, port = port, protect_args = protect_args) sync(options, context, target, verbose = verbose, thorough = thorough, - session_images = session_images, preserve_jars = preserve_jars, - dry_run = dry_run, rev = rev, afp_root = afp_root, - afp_rev = afp_rev) + purge_heaps = purge_heaps, session_images = session_images, preserve_jars = preserve_jars, + dry_run = dry_run, rev = rev, afp_root = afp_root, afp_rev = afp_rev) } ) }