diff -r 4adee07a5e48 -r 67da045668cc src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Sun Jan 22 21:55:24 2023 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Sun Jan 22 21:58:04 2023 +0100 @@ -25,33 +25,39 @@ override def toString: String = isabelle_home.toString - if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) + if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) { error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT") + } /* static system */ def bash( - script: String, - redirect: Boolean = false, - echo: Boolean = false, - strict: Boolean = true): Process_Result = + script: String, + redirect: Boolean = false, + echo: Boolean = false, + strict: Boolean = true + ): Process_Result = { progress.bash( "export USER_HOME=" + File.bash_path(user_home) + "\n" + Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script, env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict) + } def apply( - cmdline: String, - redirect: Boolean = false, - echo: Boolean = false, - strict: Boolean = true): Process_Result = + cmdline: String, + redirect: Boolean = false, + echo: Boolean = false, + strict: Boolean = true + ): Process_Result = { bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict) + } - def resolve_components(echo: Boolean): Unit = + def resolve_components(echo: Boolean): Unit = { other_isabelle( "env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) + " isabelle components -a", redirect = true, echo = echo).check + } def getenv(name: String): String = other_isabelle("getenv -b " + Bash.string(name)).check.out @@ -87,13 +93,15 @@ def clean_settings(): Boolean = if (!etc_settings.is_file) true else if (File.read(etc_settings).startsWith("# generated by Isabelle")) { - etc_settings.file.delete; true + etc_settings.file.delete + true } else false def init_settings(settings: List[String]): Unit = { - if (!clean_settings()) + if (!clean_settings()) { error("Cannot proceed with existing user settings file: " + etc_settings) + } Isabelle_System.make_directory(etc_settings.dir) File.write(etc_settings,