diff -r d44e2d1ca84f -r 4c2aaf60c22c src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Wed Jan 25 15:18:06 2023 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Wed Jan 25 15:26:23 2023 +0100 @@ -139,6 +139,18 @@ } + def init( + other_settings: List[String] = init_components(), + fresh: Boolean = false, + echo: Boolean = false + ): Unit = { + init_settings(other_settings) + resolve_components(echo = echo) + scala_build(fresh = fresh, echo = echo) + } + + + /* cleanup */ def cleanup(): Unit = {