more general dirs for Sync.sync;

--- a/src/Pure/Admin/build_history.scala	Sat May 25 12:20:57 2024 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat May 25 17:22:05 2024 +0200
@@ -167,7 +167,7 @@
 
     val isabelle_directory = directory(root)
     val (afp_directory, afp_build_args) =
-      if (afp) (Some(directory(root + Path.explode("AFP"))), List("-d", "~~/AFP/thys"))
+      if (afp) (Some(directory(root + Path.explode("AFP"))), List("-d", "~~/dirs/AFP/thys"))
       else (None, Nil)
 
 
@@ -548,7 +548,7 @@
     ): Unit = {
       Sync.sync(ssh.options, Rsync.Context(progress = progress, ssh = ssh), target,
         thorough = accurate, preserve_jars = !accurate,
-        rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
+        rev = rev, dirs = Sync.afp_dirs(if (afp) afp_repos else None, rev = afp_rev))
     }
 
     if (!shared_isabelle_self) sync(isabelle_self)

--- a/src/Pure/Build/build.scala	Sat May 25 12:20:57 2024 +0200
+++ b/src/Pure/Build/build.scala	Sat May 25 17:22:05 2024 +0200
@@ -599,7 +599,6 @@
     build_options: List[Options.Spec] = Nil,
     build_id: String = "",
     isabelle_home: Path = Path.current,
-    afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
     quiet: Boolean = false,
     verbose: Boolean = false
@@ -607,7 +606,6 @@
     val options = build_options ::: Options.Spec.eq("build_hostname", host.name) :: host.options
     ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_worker" +
       if_proper(build_id, " -B " + Bash.string(build_id)) +
-      if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
       dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
       if_proper(host.numa, " -N") + " -j" + host.jobs +
       Options.Spec.bash_strings(options, bg = true) +
@@ -619,7 +617,6 @@
     options: Options,
     build_id: String = "",
     progress: Progress = new Progress,
-    afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Option[Int] = None
@@ -634,18 +631,19 @@
 
         val build_master = find_builds(build_database, build_id, builds.filter(_.active))
 
+        val more_dirs = List(Path.ISABELLE_HOME + Sync.DIRS).filter(Sessions.is_session_dir(_))
+
         val sessions_structure =
-          Sessions.load_structure(build_options, dirs = AFP.main_dirs(afp_root) ::: dirs).
+          Sessions.load_structure(build_options, dirs = more_dirs ::: dirs).
             selection(Sessions.Selection(sessions = build_master.sessions))
 
         val build_deps =
           Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
 
         val build_context =
-          Context(store, build_deps, engine = engine, afp_root = afp_root,
-            hostname = hostname(build_options), numa_shuffling = numa_shuffling,
-            build_uuid = build_master.build_uuid, build_start = Some(build_master.start),
-            jobs = max_jobs.getOrElse(1))
+          Context(store, build_deps, engine = engine, hostname = hostname(build_options),
+            numa_shuffling = numa_shuffling, build_uuid = build_master.build_uuid,
+            build_start = Some(build_master.start), jobs = max_jobs.getOrElse(1))
 
         engine.run_build_process(build_context, progress, server)
       }
@@ -655,7 +653,6 @@
   val isabelle_tool3 = Isabelle_Tool("build_worker", "start worker for session build process",
     Scala_Project.here,
     { args =>
-      var afp_root: Option[Path] = None
       var build_id = ""
       var numa_shuffling = false
       val dirs = new mutable.ListBuffer[Path]
@@ -670,7 +667,6 @@
 Usage: isabelle build_worker [OPTIONS]
 
   Options are:
-    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
     -B UUID      existing UUID for build process (default: from database)
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -d DIR       include session directory
@@ -679,7 +675,6 @@
     -q           quiet mode: no progress
     -v           verbose
 """,
-        "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "B:" -> (arg => build_id = arg),
         "N" -> (_ => numa_shuffling = true),
         "d:" -> (arg => dirs += Path.explode(arg)),
@@ -701,7 +696,6 @@
           build_worker(options,
             build_id = build_id,
             progress = progress,
-            afp_root = afp_root,
             dirs = dirs.toList,
             numa_shuffling = Host.numa_check(progress, numa_shuffling),
             max_jobs = max_jobs)

--- a/src/Pure/Build/build_cluster.scala	Sat May 25 12:20:57 2024 +0200
+++ b/src/Pure/Build/build_cluster.scala	Sat May 25 17:22:05 2024 +0200
@@ -174,9 +174,6 @@
     val build_cluster_identifier: String = options.string("build_cluster_identifier")
     val build_cluster_root: Path = Path.explode(options.string("build_cluster_root"))
     val built_cluster_isabelle_home: Path = build_cluster_root + Path.explode("isabelle")
-    val build_cluster_afp_root: Option[Path] =
-      if (build_context.afp_root.isEmpty) None
-      else Some(built_cluster_isabelle_home + Path.explode("AFP"))
 
     lazy val build_cluster_isabelle: Other_Isabelle =
       Other_Isabelle(built_cluster_isabelle_home,
@@ -184,9 +181,9 @@
 
     def sync(): Other_Isabelle = {
       Sync.sync(options, Rsync.Context(ssh = ssh), built_cluster_isabelle_home,
-        afp_root = build_context.afp_root,
         purge_heaps = true,
-        preserve_jars = true)
+        preserve_jars = true,
+        dirs = Sync.afp_dirs(build_context.afp_root))
       build_cluster_isabelle
     }
 
@@ -215,7 +212,6 @@
           build_options = build_options.toList,
           build_id = build_context.build_uuid,
           isabelle_home = built_cluster_isabelle_home,
-          afp_root = build_cluster_afp_root,
           dirs = Path.split(host.dirs).map(build_cluster_isabelle.expand_path),
           quiet = true)
       build_cluster_isabelle.bash(script).check

--- a/src/Pure/Tools/sync.scala	Sat May 25 12:20:57 2024 +0200
+++ b/src/Pure/Tools/sync.scala	Sat May 25 17:22:05 2024 +0200
@@ -34,6 +34,24 @@
 
   /* sync */
 
+  val DIRS: Path = Path.basic("dirs")
+  val DIRS_ROOTS: Path = DIRS + Sessions.ROOTS
+
+  sealed case class Dir(name: String, root: Path, path: Path = Path.current, rev: String = "") {
+    lazy val hg: Mercurial.Repository = Mercurial.repository(root)
+    def check(): Unit = hg
+
+    def source: Path = root + path
+    def target: Path = DIRS + Path.basic(name)
+    def roots_entry: String = ((if (name.isEmpty) Path.parent else Path.basic(name)) + path).implode
+  }
+
+  def afp_dir(base_dir: Path = AFP.BASE, rev: String = ""): Dir =
+    Dir("AFP", base_dir, path = AFP.main_dir(base_dir = Path.current), rev = rev)
+
+  def afp_dirs(root: Option[Path] = None, rev: String = ""): List[Dir] =
+    root.toList.map(base_dir => afp_dir(base_dir = base_dir, rev = rev))
+
   def sync(options: Options, context: Rsync.Context, target: Path,
     thorough: Boolean = false,
     purge_heaps: Boolean = false,
@@ -41,13 +59,23 @@
     preserve_jars: Boolean = false,
     dry_run: Boolean = false,
     rev: String = "",
-    afp_root: Option[Path] = None,
-    afp_rev: String = ""
+    dirs: List[Dir] = Nil
   ): Unit = {
     val progress = context.progress
 
     val self = Mercurial.self_repository()
-    val afp = afp_root.map(Mercurial.repository(_))
+    dirs.foreach(_.check())
+
+    val sync_dirs: List[Dir] = {
+      val m =
+        Multi_Map.from(
+          for (dir <- dirs.iterator if dir.name.nonEmpty) yield dir.name -> dir.root.canonical)
+      for ((name, roots) <- m.iterator_list if roots.length > 1) {
+        error("Incoherent sync directory " + quote(name) + ":\n" +
+          cat_lines(roots.reverse.map(p => "  " + p.toString)))
+      }
+      Library.distinct(dirs, (d1: Dir, d2: Dir) => d1.name == d2.name)
+    }
 
     val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
 
@@ -60,18 +88,20 @@
 
     progress.echo("\n* Isabelle:", verbose = true)
     val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
+    val filter_dirs = sync_dirs.map(dir => "protect /" + dir.target.implode)
     synchronize(self, target, rev,
       contents = List(File.content(Path.explode("etc/ISABELLE_ID"), self.id(rev = rev))),
-      filter = filter_heaps ::: List("protect /AFP"))
+      filter = filter_heaps ::: filter_dirs)
 
-    for (src <- afp) {
-      progress.echo("\n* AFP:", verbose = true)
-      synchronize(src, target + Path.explode("AFP"), afp_rev)
+    context.ssh.make_directory(target + DIRS)
+    context.ssh.write(target + DIRS_ROOTS, Library.terminate_lines(dirs.map(_.roots_entry)))
+
+    for (dir <- sync_dirs) {
+      progress.echo("\n* " + dir.name + ":", verbose = true)
+      synchronize(dir.hg, target + dir.target, dir.rev)
     }
 
-    val images =
-      find_images(options, session_images,
-        dirs = afp_root.map(_ + Path.explode("thys")).toList)
+    val images = find_images(options, session_images, dirs = dirs.map(_.source))
     if (images.nonEmpty) {
       progress.echo("\n* Session images:", verbose = true)
       val heaps = context.target(target + Path.explode("heaps")) + "/"
@@ -143,7 +173,7 @@
           val context = Rsync.Context(progress = progress, ssh = ssh, stats = verbose)
           sync(options, context, target, thorough = thorough, 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)
+            rev = rev, dirs = afp_dirs(afp_root, afp_rev))
         }
       }
     )