# HG changeset patch # User wenzelm # Date 1674649003 -3600 # Node ID d3437203c1df63683a8cd6c49576ae268a396258 # Parent 6e2c6ccc5dc02e6d62b7463b96a61381a3a4c7f8 clarified parameters (again); diff -r 6e2c6ccc5dc0 -r d3437203c1df src/Pure/Admin/other_isabelle.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) } diff -r 6e2c6ccc5dc0 -r d3437203c1df src/Pure/System/components.scala --- 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")