clarified parameters (again);
authorwenzelm
Wed, 25 Jan 2023 13:16:43 +0100
changeset 77090 d3437203c1df
parent 77088 6e2c6ccc5dc0
child 77091 15e710116a16
clarified parameters (again);
src/Pure/Admin/other_isabelle.scala
src/Pure/System/components.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Wed Jan 25 13:16:43 2023 +0100
@@ -89,15 +89,17 @@
 
   def init_components(
     component_repository: String = Components.default_component_repository,
+    components_base: String = Components.standard_components_base,
     catalogs: List[String] = Components.default_catalogs,
     components: List[String] = Nil
   ): List[String] = {
     val admin = Components.admin(Path.ISABELLE_HOME).implode
-    val components_base = quote("${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}")
 
     ("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
-    catalogs.map(name => "init_components " + components_base + " " + quote(admin + "/" + name)) :::
-    components.map(name => "init_component " + components_base + "/" + name)
+    catalogs.map(name =>
+      "init_components " + quote(components_base) + " " + quote(admin + "/" + name)) :::
+    components.map(name =>
+      "init_component " + quote(components_base) + "/" + name)
   }
 
 
--- a/src/Pure/System/components.scala	Tue Jan 24 23:05:32 2023 +0100
+++ b/src/Pure/System/components.scala	Wed Jan 25 13:16:43 2023 +0100
@@ -39,6 +39,7 @@
     Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
 
   val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
+  val standard_components_base: String = "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}"
 
   val default_catalogs: List[String] = List("main")
   val optional_catalogs: List[String] = List("main", "optional")