clarified signature: more operations;
authorwenzelm
Thu, 20 Jul 2023 12:38:00 +0200
changeset 78417 01f61cf796e0
parent 78416 f26eba6281b1
child 78418 bc62be4144e6
clarified signature: more operations;
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 */