# HG changeset patch
# User wenzelm
# Date 1678719211 -3600
# Node ID a538dab533ef4befa6976157527b7af77ad57b8e
# Parent  582a7db1da3727b4ffab2e3b928c67c2181c9d44
clarified signature: prefer explicit types;

diff -r 582a7db1da37 -r a538dab533ef src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Mon Mar 13 15:35:15 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Mon Mar 13 15:53:31 2023 +0100
@@ -105,9 +105,7 @@
   val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
     Scala_Project.here,
     { args =>
-      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
-
-      var options = Options.init(opts = build_options)
+      var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
       val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
       val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
       val mirabelle_randomize = options.check_name("mirabelle_randomize")
diff -r 582a7db1da37 -r a538dab533ef src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Mar 13 15:35:15 2023 +0100
+++ b/src/Pure/System/options.scala	Mon Mar 13 15:53:31 2023 +0100
@@ -16,6 +16,9 @@
         case Properties.Eq(a, b) => Spec(a, Some(b))
         case _ => Spec(s)
       }
+
+    def ISABELLE_BUILD_OPTIONS: List[Spec] =
+      Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).map(make)
   }
 
   sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {
@@ -196,13 +199,13 @@
   def read_prefs(file: Path = PREFS): String =
     if (file.is_file) File.read(file) else ""
 
-  def init(prefs: String = read_prefs(file = PREFS), opts: List[String] = Nil): Options = {
+  def init(prefs: String = read_prefs(file = PREFS), specs: List[Spec] = Nil): Options = {
     var options = empty
     for {
       dir <- Components.directories()
       file = dir + OPTIONS if file.is_file
     } { options = Parsers.parse_file(options, file.implode, File.read(file)) }
-    opts.foldLeft(Parsers.parse_prefs(options, prefs))(_ + _)
+    Parsers.parse_prefs(options, prefs) ++ specs
   }
 
   def init0(): Options = init(prefs = "")
@@ -244,10 +247,7 @@
       val options = {
         val options0 = Options.init()
         val options1 =
-          if (build_options) {
-            Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
-          }
-          else options0
+          if (build_options) options0 ++ Options.Spec.ISABELLE_BUILD_OPTIONS else options0
         more_options.foldLeft(options1)(_ + _)
       }
 
diff -r 582a7db1da37 -r a538dab533ef src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Mar 13 15:35:15 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 13 15:53:31 2023 +0100
@@ -248,8 +248,6 @@
   val isabelle_tool1 = Isabelle_Tool("build", "build and manage Isabelle sessions",
     Scala_Project.here,
     { args =>
-      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
-
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var numa_shuffling = false
@@ -268,7 +266,7 @@
       var check_keywords: Set[String] = Set.empty
       var list_files = false
       var no_build = false
-      var options = Options.init(opts = build_options)
+      var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
       var verbose = false
       var exclude_sessions: List[String] = Nil
 
@@ -406,12 +404,10 @@
   val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process",
     Scala_Project.here,
     { args =>
-      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
-
       var numa_shuffling = false
       var dirs: List[Path] = Nil
       var max_jobs = 1
-      var options = Options.init(opts = build_options)
+      var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
       var verbose = false
       var build_uuid = ""
 
diff -r 582a7db1da37 -r a538dab533ef src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Mon Mar 13 15:35:15 2023 +0100
+++ b/src/Pure/Tools/server_commands.scala	Mon Mar 13 15:53:31 2023 +0100
@@ -61,7 +61,8 @@
       args: Args,
       progress: Progress = new Progress
     ) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = {
-      val options = Options.init(prefs = args.preferences, opts = args.options)
+      val options =
+        Options.init(prefs = args.preferences, specs = args.options.map(Options.Spec.make))
       val dirs = args.dirs.map(Path.explode)
 
       val session_background =