# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717519384 -7200
# Node ID 8ae6f4e8cc2ab76f27ee7eff48a192f26ef29027
# Parent  58881e1e4a759fc0128a838bbce7d24893a12cd3
allow explicit Isabelle rev in build task (e.g., for older Isabelle versions);

diff -r 58881e1e4a75 -r 8ae6f4e8cc2a src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jun 04 18:24:38 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jun 04 18:43:04 2024 +0200
@@ -1162,6 +1162,7 @@
     sessions: List[String] = Nil,
     prefs: List[Options.Spec] = Nil,
     exclude_sessions: List[String] = Nil,
+    rev: String = "",
     progress: Progress = new Progress
   ): UUID.T = {
     val id = UUID.random()
@@ -1179,7 +1180,7 @@
         val rsync_context = Rsync.Context(ssh = ssh, chmod = "g+rwx")
         progress.echo("Transferring repositories...")
         Sync.sync(store.options, rsync_context, context.isabelle_dir, preserve_jars = true,
-          dirs = Sync.afp_dirs(afp_root))
+          dirs = Sync.afp_dirs(afp_root), rev = rev)
         ssh.execute("chmod g+rwx " + File.bash_path(context.dir))
 
         if (progress.stopped) {
@@ -1274,6 +1275,7 @@
       val session_groups = new mutable.ListBuffer[String]
       var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
       var prefs: List[Options.Spec] = Nil
+      var rev = ""
       val exclude_sessions = new mutable.ListBuffer[String]
 
       val getopts = Getopts("""
@@ -1293,6 +1295,7 @@
     -g NAME      select session group NAME
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p OPTIONS   comma-separated preferences for build process
+    -r REV       explicit revision (default: state of working directory)
     -x NAME      exclude session NAME and all descendants
 
   Submit build task on SSH server. Notable system options:
@@ -1311,6 +1314,7 @@
         "g:" -> (arg => session_groups += arg),
         "o:" -> (arg => options = options + arg),
         "p:" -> (arg => prefs = Options.Spec.parse(arg)),
+        "r:" -> (arg => rev = arg),
         "x:" -> (arg => exclude_sessions += arg))
 
       val sessions = getopts(args)
@@ -1322,7 +1326,7 @@
         exclude_session_groups = exclude_session_groups.toList, all_sessions = all_sessions,
         build_heap = build_heap, clean_build = clean_build, export_files = export_files,
         fresh_build = fresh_build, session_groups = session_groups.toList, sessions = sessions,
-        prefs = prefs, exclude_sessions = exclude_sessions.toList, progress = progress)
+        prefs = prefs, rev = rev, exclude_sessions = exclude_sessions.toList, progress = progress)
     })
 }