more robust type, with explicit default;

--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -42,7 +42,7 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1,
+    max_jobs: Option[Int] = None,
   ): Build.Results = {
     require(!selection.requirements)
     Isabelle_System.make_directory(output_dir)
@@ -123,7 +123,7 @@
       var all_sessions = false
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
-      var max_jobs = 1
+      var max_jobs: Option[Int] = None
       var verbose = false
       var exclude_sessions: List[String] = Nil
 
@@ -174,7 +174,7 @@
         "a" -> (_ => all_sessions = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+        "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
         "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
         "o:" -> (arg => options = options + arg),
         "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),

--- a/src/Pure/Admin/build_doc.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Admin/build_doc.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -14,7 +14,7 @@
     options: Options,
     progress: Progress = new Progress,
     all_docs: Boolean = false,
-    max_jobs: Int = 1,
+    max_jobs: Option[Int] = None,
     sequential: Boolean = false,
     docs: List[String] = Nil,
     view: Boolean = false
@@ -85,7 +85,7 @@
       { args =>
         var view = false
         var all_docs = false
-        var max_jobs = 1
+        var max_jobs: Option[Int] = None
         var sequential = false
         var options = Options.init()
 
@@ -105,7 +105,7 @@
 """,
             "V" -> (_ => view = true),
             "a" -> (_ => all_docs = true),
-            "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+            "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
             "o:" -> (arg => options = options + arg),
             "s" -> (_ => sequential = true))
 

--- a/src/Pure/Admin/ci_build.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Admin/ci_build.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -179,7 +179,7 @@
           progress = progress,
           clean_build = config.clean,
           numa_shuffling = profile.numa,
-          max_jobs = profile.jobs,
+          max_jobs = Some(profile.jobs),
           dirs = config.include,
           select_dirs = config.select)
       }

--- a/src/Pure/Build/build.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Build/build.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -35,7 +35,7 @@
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
     build_heap: Boolean = false,
-    max_jobs: Int = 1,
+    max_jobs: Option[Int] = None,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => (),
@@ -49,7 +49,8 @@
 
     def sessions_structure: isabelle.Sessions.Structure = build_deps.sessions_structure
 
-    def worker_active: Boolean = max_jobs > 0
+    def jobs: Int = max_jobs.getOrElse(1)
+    def worker_active: Boolean = jobs > 0
   }
 
 
@@ -160,7 +161,7 @@
     select_dirs: List[Path] = Nil,
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1,
+    max_jobs: Option[Int] = None,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
@@ -328,7 +329,7 @@
       var export_files = false
       var fresh_build = false
       val session_groups = new mutable.ListBuffer[String]
-      var max_jobs = 1
+      var max_jobs: Option[Int] = None
       var check_keywords: Set[String] = Set.empty
       var list_files = false
       var no_build = false
@@ -391,7 +392,7 @@
         "e" -> (_ => export_files = true),
         "f" -> (_ => fresh_build = true),
         "g:" -> (arg => session_groups += arg),
-        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+        "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
         "k:" -> (arg => check_keywords = check_keywords + arg),
         "l" -> (_ => list_files = true),
         "n" -> (_ => no_build = true),
@@ -601,7 +602,7 @@
     afp_root: Option[Path] = None,
     dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1
+    max_jobs: Option[Int] = None
   ): Results = {
     val build_engine = Engine(engine_name(options))
     val store = build_engine.build_store(options)
@@ -637,7 +638,7 @@
       var build_id = ""
       var numa_shuffling = false
       val dirs = new mutable.ListBuffer[Path]
-      var max_jobs = 1
+      var max_jobs: Option[Int] = None
       var options =
         Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS :::
           List(
@@ -663,7 +664,7 @@
         "B:" -> (arg => build_id = arg),
         "N" -> (_ => numa_shuffling = true),
         "d:" -> (arg => dirs += Path.explode(arg)),
-        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+        "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
         "o:" -> (arg => options = options + arg),
         "q" -> (_ => quiet = true),
         "v" -> (_ => verbose = true))

--- a/src/Pure/Build/build_process.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -977,7 +977,7 @@
   protected def next_jobs(state: Build_Process.State): List[String] = {
     val limit = {
       if (progress.stopped) { if (build_context.master) Int.MaxValue else 0 }
-      else build_context.max_jobs - state.build_running.length
+      else build_context.jobs - state.build_running.length
     }
     if (limit > 0) state.next_ready.sortBy(_.name)(state.sessions.ordering).take(limit).map(_.name)
     else Nil

--- a/src/Pure/Build/build_schedule.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -922,11 +922,11 @@
 
     private val timing_data: Timing_Data = {
       val cluster_hosts: List[Build_Cluster.Host] =
-        if (build_context.max_jobs == 0) build_context.build_hosts
+        if (build_context.jobs == 0) build_context.build_hosts
         else {
           val local_build_host =
             Build_Cluster.Host(
-              hostname, jobs = build_context.max_jobs, numa = build_context.numa_shuffling)
+              hostname, jobs = build_context.jobs, numa = build_context.numa_shuffling)
           local_build_host :: build_context.build_hosts
         }
 
@@ -1037,7 +1037,7 @@
     override def run(): Build.Results = {
       Benchmark.benchmark_requirements(build_options)
 
-      if (build_context.max_jobs > 0) {
+      if (build_context.jobs > 0) {
         val benchmark_options = build_options.string("build_hostname") = hostname
         Benchmark.benchmark(benchmark_options, progress)
       }
@@ -1306,7 +1306,7 @@
       val build_context =
         Build.Context(store, build_engine, build_deps, afp_root = afp_root,
           build_hosts = build_hosts, hostname = Build.hostname(build_options),
-          numa_shuffling = numa_shuffling, max_jobs = 0, session_setup = session_setup,
+          numa_shuffling = numa_shuffling, max_jobs = Some(0), session_setup = session_setup,
           master = true)
 
       val cluster_hosts = build_context.build_hosts

--- a/src/Pure/Tools/profiling.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Tools/profiling.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -225,7 +225,7 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1
+    max_jobs: Option[Int] = None
   ): Results = {
     /* sessions structure */
 
@@ -313,7 +313,7 @@
         var all_sessions = false
         var dirs: List[Path] = Nil
         var session_groups: List[String] = Nil
-        var max_jobs = 1
+        var max_jobs: Option[Int] = None
         var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
         var verbose = false
         var exclude_sessions: List[String] = Nil
@@ -345,7 +345,7 @@
           "a" -> (_ => all_sessions = true),
           "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
           "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-          "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+          "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
           "o:" -> (arg => options = options + arg),
           "v" -> (_ => verbose = true),
           "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))

--- a/src/Pure/Tools/update.scala	Thu Feb 15 10:32:36 2024 +0100
+++ b/src/Pure/Tools/update.scala	Thu Feb 15 11:33:36 2024 +0100
@@ -52,7 +52,7 @@
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
-    max_jobs: Int = 1,
+    max_jobs: Option[Int] = None,
     fresh_build: Boolean = false,
     no_build: Boolean = false
   ): Build.Results = {
@@ -148,7 +148,7 @@
         var dirs: List[Path] = Nil
         var fresh_build = false
         var session_groups: List[String] = Nil
-        var max_jobs = 1
+        var max_jobs: Option[Int] = None
         var base_logics: List[String] = List(default_base_logic)
         var no_build = false
         var options = Options.init()
@@ -192,7 +192,7 @@
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "f" -> (_ => fresh_build = true),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+        "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
         "l:" -> (arg => base_logics = space_explode(',', arg)),
         "n" -> (_ => no_build = true),
         "o:" -> (arg => options = options + arg),