clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;

--- a/src/Pure/System/process_result.scala	Sat Feb 11 22:13:55 2023 +0100
+++ b/src/Pure/System/process_result.scala	Sat Feb 11 22:36:13 2023 +0100
@@ -10,6 +10,7 @@
   /* return code */
 
   object RC {
+    val undefined = -1
     val ok = 0
     val error = 1
     val failure = 2
@@ -20,6 +21,7 @@
     private def text(rc: Int): String = {
       val txt =
         rc match {
+          case `undefined` => "UNDEFINED"
           case `ok` => "OK"
           case `error` => "ERROR"
           case `failure` => "FAILURE"
@@ -40,6 +42,7 @@
     def print(rc: Int): String = "return code " + rc + text(rc)
   }
 
+  val undefined: Process_Result = Process_Result(RC.undefined)
   val ok: Process_Result = Process_Result(RC.ok)
   val error: Process_Result = Process_Result(RC.error)
   val startup_failure: Process_Result = Process_Result(RC.startup_failure)
@@ -64,6 +67,9 @@
   def ok: Boolean = rc == Process_Result.RC.ok
   def interrupted: Boolean = rc == Process_Result.RC.interrupt
 
+  def defined: Boolean = rc > Process_Result.RC.undefined
+  def strict: Process_Result = if (defined) this else copy(rc = Process_Result.RC.error)
+
   def timeout_rc: Process_Result = copy(rc = Process_Result.RC.timeout)
   def timeout: Boolean = rc == Process_Result.RC.timeout
 

--- a/src/Pure/Tools/build.scala	Sat Feb 11 22:13:55 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 22:36:13 2023 +0100
@@ -71,17 +71,15 @@
     val store: Sessions.Store,
     val deps: Sessions.Deps,
     val sessions_ok: List[String],
-    results: Map[String, Option[Process_Result]]
+    results: Map[String, Process_Result]
   ) {
     def cache: Term.Cache = store.cache
 
     def info(name: String): Sessions.Info = deps.sessions_structure(name)
     def sessions: Set[String] = results.keySet
-    def cancelled(name: String): Boolean = results(name).isEmpty
-    def apply(name: String): Process_Result = results(name).getOrElse(Process_Result.error)
-    val rc: Int =
-      results.iterator.map({ case (_, Some(r)) => r.rc case (_, None) => Process_Result.RC.error }).
-        foldLeft(Process_Result.RC.ok)(_ max _)
+    def cancelled(name: String): Boolean = !results(name).defined
+    def apply(name: String): Process_Result = results(name).strict
+    val rc: Int = results.valuesIterator.map(_.strict.rc).foldLeft(Process_Result.RC.ok)(_ max _)
     def ok: Boolean = rc == Process_Result.RC.ok
 
     def unfinished: List[String] = sessions.iterator.filterNot(apply(_).ok).toList.sorted
@@ -203,13 +201,9 @@
     case class Result(
       current: Boolean,
       output_heap: SHA1.Shasum,
-      process: Option[Process_Result]
+      process_result: Process_Result
     ) {
-      def ok: Boolean =
-        process match {
-          case None => false
-          case Some(res) => res.ok
-        }
+      def ok: Boolean = process_result.ok
     }
 
     def sleep(): Unit =
@@ -298,7 +292,7 @@
             }
 
             loop(pending - session_name, running - session_name,
-              results + (session_name -> Result(false, output_heap, Some(process_result_tail))))
+              results + (session_name -> Result(false, output_heap, process_result_tail)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
@@ -339,12 +333,12 @@
 
                 if (all_current) {
                   loop(pending - session_name, running,
-                    results + (session_name -> Result(true, output_heap, Some(Process_Result.ok))))
+                    results + (session_name -> Result(true, output_heap, Process_Result.ok)))
                 }
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
-                    results + (session_name -> Result(false, output_heap, Some(Process_Result.error))))
+                    results + (session_name -> Result(false, output_heap, Process_Result.error)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
@@ -367,7 +361,7 @@
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
-                    results + (session_name -> Result(false, output_heap, None)))
+                    results + (session_name -> Result(false, output_heap, Process_Result.undefined)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
@@ -397,7 +391,7 @@
 
       val results =
         (for ((name, result) <- build_results.iterator)
-          yield (name, result.process)).toMap
+          yield (name, result.process_result)).toMap
 
       new Results(store, build_deps, sessions_ok, results)
     }