# HG changeset patch
# User wenzelm
# Date 1754678078 -7200
# Node ID 7e8c6cf127f0cd3090a101c9c78d2f58193e7ac4
# Parent  9164cace10ca39303c4619b48aeb565c92a4c173
support private_dir for transient output;

diff -r 9164cace10ca -r 7e8c6cf127f0 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Fri Aug 08 17:26:05 2025 +0200
+++ b/src/Pure/Build/store.scala	Fri Aug 08 20:34:38 2025 +0200
@@ -13,9 +13,10 @@
 object Store {
   def apply(
     options: Options,
+    private_dir: Option[Path] = None,
     build_cluster: Boolean = false,
     cache: Rich_Text.Cache = Rich_Text.Cache.make()
-  ): Store = new Store(options, build_cluster, cache)
+  ): Store = new Store(options, private_dir, build_cluster, cache)
 
 
   /* file names */
@@ -276,6 +277,7 @@
 
 class Store private(
     val options: Options,
+    private_dir: Option[Path],
     val build_cluster: Boolean,
     val cache: Rich_Text.Cache
   ) {
@@ -288,6 +290,9 @@
 
   val ml_settings: ML_Settings = ML_Settings(options)
 
+  val private_output_dir: Option[Path] =
+    private_dir.map(dir => dir + Path.basic("heaps") + Path.basic(ml_settings.ml_identifier))
+
   val system_output_dir: Path =
     Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_settings.ml_identifier)
 
@@ -324,18 +329,19 @@
   def system_heaps: Boolean = options.bool("system_heaps")
 
   val output_dir: Path =
-    if (system_heaps) system_output_dir else user_output_dir
+    private_output_dir.getOrElse(if (system_heaps) system_output_dir else user_output_dir)
 
   val input_dirs: List[Path] =
-    if (system_heaps) List(system_output_dir)
-    else List(user_output_dir, system_output_dir)
+    private_output_dir.toList :::
+      (if (system_heaps) List(system_output_dir) else List(user_output_dir, system_output_dir))
 
   val clean_dirs: List[Path] =
-    if (system_heaps) List(user_output_dir, system_output_dir)
-    else List(user_output_dir)
+    private_output_dir.toList :::
+      (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
 
   def presentation_dir: Path =
-    if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
+    if (private_dir.isDefined) private_dir.get + Path.basic("browser_info")
+    else if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
     else Path.explode("$ISABELLE_BROWSER_INFO")