discontinue unused parameter (better done as system option);
authorwenzelm
Sat, 14 Jun 2025 21:07:09 +0200
changeset 82710 e09e986731e9
parent 82709 1008b8e7c78d
child 82711 5bd0d6a8fd7a
discontinue unused parameter (better done as system option);
src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sat Jun 14 17:10:18 2025 +0200
+++ b/src/Pure/Build/store.scala	Sat Jun 14 21:07:09 2025 +0200
@@ -14,9 +14,8 @@
   def apply(
     options: Options,
     build_cluster: Boolean = false,
-    cache: Term.Cache = Term.Cache.make(),
-    other_ml_platform: Option[String] = None
-  ): Store = new Store(options, build_cluster, cache, other_ml_platform)
+    cache: Term.Cache = Term.Cache.make()
+  ): Store = new Store(options, build_cluster, cache)
 
 
   /* file names */
@@ -278,8 +277,7 @@
 class Store private(
     val options: Options,
     val build_cluster: Boolean,
-    val cache: Term.Cache,
-    other_ml_platform: Option[String]
+    val cache: Term.Cache
   ) {
   store =>
 
@@ -289,7 +287,7 @@
   /* ML system */
 
   def ml_system: String = Isabelle_System.getenv_strict("ML_SYSTEM")
-  def ml_platform: String = other_ml_platform getOrElse Isabelle_System.getenv_strict("ML_PLATFORM")
+  def ml_platform: String = Isabelle_System.getenv_strict("ML_PLATFORM")
   def ml_identifier: String = ml_system + "_" + ml_platform