# HG changeset patch
# User wenzelm
# Date 1653942885 -7200
# Node ID 0a5f7b5da16f8663d2f30d97b3c08f7f845c33de
# Parent  99b37c39143353e7c75315a29cd5894ba1fdfdd6
clarified options;

diff -r 99b37c391433 -r 0a5f7b5da16f src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Mon May 30 20:58:45 2022 +0200
+++ b/src/Pure/Admin/afp.scala	Mon May 30 22:34:45 2022 +0200
@@ -23,7 +23,9 @@
 
   val force_partition1: List[String] = List("Category3", "HOL-ODE")
 
-  def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
+  val BASE: Path = Path.explode("$AFP_BASE")
+
+  def init(options: Options, base_dir: Path = BASE): AFP =
     new AFP(options, base_dir)
 
 
diff -r 99b37c391433 -r 0a5f7b5da16f src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala	Mon May 30 20:58:45 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Mon May 30 22:34:45 2022 +0200
@@ -64,7 +64,7 @@
 Usage: isabelle sync_repos [OPTIONS] TARGET
 
   Options are:
-    -A ROOT      include AFP with given root directory
+    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
     -J           preserve *.jar files
     -C           clean all unknown/ignored files on target
                  (implies -n for testing; use option -f to confirm)
@@ -81,13 +81,13 @@
 
    * quick testing
 
-      isabelle sync_repos -A '$AFP_BASE' -J -C testmachine:test/isabelle_afp
+      isabelle sync_repos -A: -J -C testmachine:test/isabelle_afp
 
    * accurate testing
 
-      isabelle sync_repos -A '$AFP_BASE' -T -C testmachine:test/isabelle_afp
+      isabelle sync_repos -A: -T -C testmachine:test/isabelle_afp
 """,
-          "A:" -> (arg => afp_root = Some(Path.explode(arg))),
+          "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
           "J" -> (_ => preserve_jars = true),
           "C" -> { _ => clean = true; dry_run = true },
           "T" -> (_ => thorough = true),