src/Pure/Build/store.scala
changeset 82718 e1a8753eaad7
parent 82716 6e33d46b1400
child 82720 956ecf2c07a0
--- a/src/Pure/Build/store.scala	Sun Jun 15 13:40:03 2025 +0200
+++ b/src/Pure/Build/store.scala	Sun Jun 15 15:19:03 2025 +0200
@@ -278,16 +278,24 @@
     val options: Options,
     val build_cluster: Boolean,
     val cache: Term.Cache
-  ) extends ML_Settings.System() {
+  ) {
   store =>
 
   override def toString: String = "Store(output_dir = " + output_dir.absolute + ")"
 
 
-  /* directories */
+  /* ML system settings */
+
+  val ml_settings: ML_Settings = ML_Settings.system()
 
-  val system_output_dir: Path = Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_identifier)
-  val user_output_dir: Path = Path.variable("ISABELLE_HEAPS") + Path.basic(ml_identifier)
+  val system_output_dir: Path =
+    Path.variable("ISABELLE_HEAPS_SYSTEM") + Path.basic(ml_settings.ml_identifier)
+
+  val user_output_dir: Path =
+    Path.variable("ISABELLE_HEAPS") + Path.basic(ml_settings.ml_identifier)
+
+
+  /* directories */
 
   def system_heaps: Boolean = options.bool("system_heaps")