# HG changeset patch
# User wenzelm
# Date 1689849480 -7200
# Node ID 01f61cf796e00750a353e55541f7c2df305d8e84
# Parent  f26eba6281b161e1e11fe2249e514b09191cca3a
clarified signature: more operations;

diff -r f26eba6281b1 -r 01f61cf796e0 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Thu Jul 20 12:29:57 2023 +0200
+++ b/src/Pure/Admin/afp.scala	Thu Jul 20 12:38:00 2023 +0200
@@ -25,6 +25,8 @@
 
   val BASE: Path = Path.explode("$AFP_BASE")
 
+  def main_dir(base_dir: Path = BASE): Path = base_dir + Path.explode("thys")
+
   def init(options: Options, base_dir: Path = BASE): AFP =
     new AFP(options, base_dir)
 
@@ -68,7 +70,7 @@
 class AFP private(options: Options, val base_dir: Path) {
   override def toString: String = base_dir.expand.toString
 
-  val main_dir: Path = base_dir + Path.explode("thys")
+  val main_dir: Path = AFP.main_dir(base_dir = base_dir)
 
 
   /* metadata */