# HG changeset patch # User wenzelm # Date 1762001799 -3600 # Node ID 0f9bae334ac6c143a494199dd75cb34b04f2a392 # Parent 5c70d1c27a2e73cd3db8ad74fd05cdb56fba0f8c more uniform Isabelle_System.default_logic, with subtle change of semantics due to getenv_strict; diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Nov 01 13:56:39 2025 +0100 @@ -110,7 +110,7 @@ val context = Build_Release.Release_Context(target_dir, progress = progress) Build_Release.build_release_archive(context, rev) Build_Release.build_release(logger.options, context, afp_rev = afp_rev, - build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")), + build_sessions = List(Isabelle_System.default_logic()), website = Some(website_dir)) } ) diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/ML/ml_console.scala Sat Nov 01 13:56:39 2025 +0100 @@ -14,7 +14,7 @@ Command_Line.tool { var dirs: List[Path] = Nil var include_sessions: List[String] = Nil - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var logic = Isabelle_System.default_logic() var modes: List[String] = Nil var no_build = false var options = Options.init() diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/ML/ml_process.scala Sat Nov 01 13:56:39 2025 +0100 @@ -135,7 +135,7 @@ { args => var dirs: List[Path] = Nil var eval_args: List[String] = Nil - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var logic = Isabelle_System.default_logic() var modes: List[String] = Nil var options = Options.init() diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/Tools/docker_build.scala --- a/src/Pure/Tools/docker_build.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/Tools/docker_build.scala Sat Nov 01 13:56:39 2025 +0100 @@ -10,7 +10,6 @@ object Docker_Build { private val default_base = "ubuntu:22.04" private val default_work_dir = Path.current - private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r @@ -34,7 +33,7 @@ app_archive: String, base: String = default_base, work_dir: Path = default_work_dir, - logic: String = default_logic, + logic: String = Isabelle_System.default_logic(), no_build: Boolean = false, entrypoint: Boolean = false, output: Option[Path] = None, @@ -120,7 +119,7 @@ var base = default_base var entrypoint = false var work_dir = default_work_dir - var logic = default_logic + var logic = Isabelle_System.default_logic() var no_build = false var output: Option[Path] = None var more_packages: List[String] = Nil @@ -137,7 +136,8 @@ package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """) -W DIR working directory that is accessible to docker, potentially via snap (default: """ + default_work_dir + """) - -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) + -l NAME default logic (default ISABELLE_LOGIC=""" + + quote(Isabelle_System.default_logic()) + """) -n no docker build -o FILE output generated Dockerfile -p NAME additional Ubuntu package diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/Tools/mkroot.scala --- a/src/Pure/Tools/mkroot.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/Tools/mkroot.scala Sat Nov 01 13:56:39 2025 +0100 @@ -30,7 +30,7 @@ Isabelle_System.make_directory(session_dir) val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName - val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC") + val parent = proper_string(session_parent) getOrElse Isabelle_System.default_logic() val root_path = session_dir + Sessions.ROOT if (root_path.file.exists) error("Cannot overwrite existing " + root_path) diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/Tools/process_theories.scala --- a/src/Pure/Tools/process_theories.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/Tools/process_theories.scala Sat Nov 01 13:56:39 2025 +0100 @@ -152,7 +152,7 @@ var unicode_symbols = false val dirs = new mutable.ListBuffer[Path] val files = new mutable.ListBuffer[Path] - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var logic = Isabelle_System.default_logic() var margin = Pretty.default_margin var options = Options.init() var verbose = false diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Pure/Tools/update_tool.scala --- a/src/Pure/Tools/update_tool.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Pure/Tools/update_tool.scala Sat Nov 01 13:56:39 2025 +0100 @@ -40,8 +40,6 @@ upd(Markup.Language.outer, xml) } - def default_base_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC") - def update(options: Options, update_options: List[Options.Spec], selection: Sessions.Selection = Sessions.Selection.empty, @@ -150,7 +148,7 @@ var fresh_build = false var session_groups: List[String] = Nil var max_jobs: Option[Int] = None - var base_logics: List[String] = List(default_base_logic) + var base_logics: List[String] = List(Isabelle_System.default_logic()) var no_build = false var options = Options.init() var update_options: List[Options.Spec] = Nil @@ -173,7 +171,7 @@ -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) -l NAMES comma-separated list of base logics, to remain unchanged - (default: """ + quote(default_base_logic) + """) + (default: """ + quote(Isabelle_System.default_logic()) + """) -n no build -- take existing session build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -u OPT override "update" option for selected sessions diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Tools/VSCode/src/component_vscode_extension.scala --- a/src/Tools/VSCode/src/component_vscode_extension.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Tools/VSCode/src/component_vscode_extension.scala Sat Nov 01 13:56:39 2025 +0100 @@ -13,10 +13,8 @@ object Component_VSCode { /* build grammar */ - def default_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC") - def build_grammar(options: Options, build_dir: Path, - logic: String = default_logic, + logic: String = Isabelle_System.default_logic(), dirs: List[Path] = Nil, progress: Progress = new Progress ): Unit = { @@ -183,7 +181,7 @@ def build_extension(options: Options, target_dir: Path = Path.current, - logic: String = default_logic, + logic: String = Isabelle_System.default_logic(), dirs: List[Path] = Nil, progress: Progress = new Progress ): Unit = { @@ -282,7 +280,7 @@ { args => var target_dir = Path.current var dirs: List[Path] = Nil - var logic = default_logic + var logic = Isabelle_System.default_logic() val getopts = Getopts(""" Usage: isabelle component_vscode_extension @@ -290,7 +288,8 @@ Options are: -D DIR target directory (default ".") -d DIR include session directory - -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) + -l NAME logic session name (default ISABELLE_LOGIC=""" + + quote(Isabelle_System.default_logic()) + """) Build the Isabelle/VSCode extension as component, for inclusion into the local VSCodium configuration. diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Tools/VSCode/src/language_server.scala --- a/src/Tools/VSCode/src/language_server.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Tools/VSCode/src/language_server.scala Sat Nov 01 13:56:39 2025 +0100 @@ -26,7 +26,7 @@ class Language_Server( val channel: Channel, val options: Options, - session_name: String = Isabelle_System.getenv("ISABELLE_LOGIC"), + session_name: String = Isabelle_System.default_logic(), include_sessions: List[String] = Nil, session_dirs: List[Path] = Nil, session_ancestor: Option[String] = None, diff -r 5c70d1c27a2e -r 0f9bae334ac6 src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Sat Nov 01 00:04:57 2025 +0100 +++ b/src/Tools/VSCode/src/vscode_main.scala Sat Nov 01 13:56:39 2025 +0100 @@ -269,7 +269,7 @@ var logic_requirements = false val dirs = new mutable.ListBuffer[Path] val include_sessions = new mutable.ListBuffer[String] - var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var logic = Isabelle_System.default_logic() var modes: List[String] = Nil var no_build = false var options = Options.init() @@ -285,7 +285,7 @@ -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + - quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """) + quote(Isabelle_System.default_logic()) + """) -m MODE add print mode for output -n no build of session image on startup -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)