src/Pure/Admin/afp.scala

--- a/src/Pure/Admin/afp.scala	Thu Jul 20 12:44:46 2023 +0200
+++ b/src/Pure/Admin/afp.scala	Thu Jul 20 12:55:47 2023 +0200
@@ -27,6 +27,12 @@
 
   def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys")
 
+  def make_dirs(afp_root: Option[Path]): List[Path] =
+    afp_root match {
+      case None => Nil
+      case Some(base_dir) => List(main_dir(base_dir = base_dir))
+    }
+
   def init(options: Options, base_dir: Path = BASE): AFP =
     new AFP(options, base_dir)