more uniform Isabelle_System.default_logic, with subtle change of semantics due to getenv_strict;
--- 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))
}
)
--- 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()
--- 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()
--- 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
--- 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)
--- 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
--- 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
--- 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.
--- 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,
--- 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)