# HG changeset patch
# User wenzelm
# Date 1676129909 -3600
# Node ID 629dce95bb5cbaec14f5d2c294fee6dc7b1e329a
# Parent  7c89e848bd18d74b31530edafe28d0900155f677
clarified signature: avoid adhoc constants;

diff -r 7c89e848bd18 -r 629dce95bb5c src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Feb 11 14:24:20 2023 +0100
+++ b/src/Pure/PIDE/prover.scala	Sat Feb 11 16:38:29 2023 +0100
@@ -138,7 +138,7 @@
       terminate_process()
       process_result.join
       stdout.join
-      exit_message(Process_Result(127))
+      exit_message(Process_Result.startup_failure)
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
diff -r 7c89e848bd18 -r 629dce95bb5c src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Feb 11 14:24:20 2023 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Feb 11 16:38:29 2023 +0100
@@ -727,7 +727,7 @@
         {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
-          case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
+          case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result.ok))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)
diff -r 7c89e848bd18 -r 629dce95bb5c src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Sat Feb 11 14:24:20 2023 +0100
+++ b/src/Pure/System/process_result.scala	Sat Feb 11 16:38:29 2023 +0100
@@ -13,6 +13,7 @@
     val ok = 0
     val error = 1
     val failure = 2
+    val startup_failure = 127
     val interrupt = 130
     val timeout = 142
 
@@ -38,6 +39,10 @@
     def print_long(rc: Int): String = "Return code: " + rc + text(rc)
     def print(rc: Int): String = "return code " + rc + text(rc)
   }
+
+  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)
 }
 
 final case class Process_Result(
diff -r 7c89e848bd18 -r 629dce95bb5c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 14:24:20 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 16:38:29 2023 +0100
@@ -118,7 +118,7 @@
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def info(name: String): Sessions.Info = results(name)._2
-    def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
+    def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result.error)
     val rc: Int =
       results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
         foldLeft(Process_Result.RC.ok)(_ max _)
@@ -382,13 +382,13 @@
                 if (all_current) {
                   loop(pending - session_name, running,
                     results +
-                      (session_name -> Result(true, output_heap, Some(Process_Result(0)), info)))
+                      (session_name -> Result(true, output_heap, Some(Process_Result.ok), info)))
                 }
                 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(1)), info)))
+                      (session_name -> Result(false, output_heap, Some(Process_Result.error), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")