clarified signature;

--- a/src/HOL/Tools/Nitpick/kodkod.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -20,7 +20,7 @@
 
   sealed case class Result(rc: Int, out: String, err: String)
   {
-    def ok: Boolean = rc == 0
+    def ok: Boolean = rc == Process_Result.RC.ok
     def check: String =
       if (ok) out else error(if (err.isEmpty) "Error" else err)
 
@@ -62,7 +62,7 @@
 
     class Exec_Context extends Context
     {
-      private var rc = 0
+      private var rc = Process_Result.RC.ok
       private val out = new StringBuilder
       private val err = new StringBuilder
 
@@ -106,7 +106,7 @@
         else {
           Some(Event_Timer.request(Time.now() + timeout) {
             context.error("Ran out of time")
-            context.return_code(2)
+            context.return_code(Process_Result.RC.failure)
             executor_kill()
           })
         }
@@ -118,10 +118,10 @@
 
       if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
         context.error("Error: trailing tokens")
-        context.exit(1)
+        context.exit(Process_Result.RC.error)
       }
       if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) {
-        context.exit(1)
+        context.exit(Process_Result.RC.error)
       }
     }
     catch {

--- a/src/Pure/Admin/build_history.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -525,8 +525,8 @@
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
-      val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
-      if (rc != 0 && exit_code) sys.exit(rc)
+      val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc }
+      if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc)
     }
   }
 

--- a/src/Pure/Admin/ci_profile.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -17,8 +17,8 @@
   case class Result(rc: Int)
   case object Result
   {
-    def ok: Result = Result(0)
-    def error: Result = Result(1)
+    def ok: Result = Result(Process_Result.RC.ok)
+    def error: Result = Result(Process_Result.RC.error)
   }
 
   private def build(options: Options): (Build.Results, Time) =

--- a/src/Pure/General/ssh.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/General/ssh.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -302,10 +302,10 @@
 
       val rc =
         try { exit_status.join }
-        catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
+        catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
 
       close()
-      if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
+      if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)
     }

--- a/src/Pure/ML/ml_console.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/ML/ml_console.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -60,7 +60,7 @@
           progress.interrupt_handler {
             Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
           }
-        if (rc != 0) sys.exit(rc)
+        if (rc != Process_Result.RC.ok) sys.exit(rc)
       }
 
       // process loop
@@ -77,7 +77,7 @@
       POSIX_Interrupt.handler { process.interrupt() } {
         new TTY_Loop(process.stdin, process.stdout).join()
         val rc = process.join()
-        if (rc != 0) sys.exit(rc)
+        if (rc != Process_Result.RC.ok) sys.exit(rc)
       }
     }
   }

--- a/src/Pure/System/bash.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/System/bash.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -230,7 +230,7 @@
 
       val rc =
         try { join() }
-        catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
+        catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt }
 
       watchdog_thread.foreach(_.cancel())
 
@@ -238,7 +238,7 @@
       out_lines.join
       err_lines.join
 
-      if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
+      if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }

--- a/src/Pure/System/command_line.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/System/command_line.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -26,7 +26,7 @@
     val thread =
       Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
         val rc =
-          try { body; 0 }
+          try { body; Process_Result.RC.ok }
           catch {
             case exn: Throwable =>
               Output.error_message(Exn.print(exn))

--- a/src/Pure/System/getopts.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/System/getopts.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -33,7 +33,7 @@
   def usage(): Nothing =
   {
     Output.writeln(usage_text, stdout = true)
-    sys.exit(1)
+    sys.exit(Process_Result.RC.error)
   }
 
   private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)

--- a/src/Pure/System/process_result.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/System/process_result.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -8,30 +8,39 @@
 
 object Process_Result
 {
-  def print_return_code(rc: Int): String = "Return code: " + rc + rc_text(rc)
-  def print_rc(rc: Int): String = "return code " + rc + rc_text(rc)
+  /* return code */
+
+  object RC
+  {
+    val ok = 0
+    val error = 1
+    val failure = 2
+    val interrupt = 130
+    val timeout = 142
 
-  def rc_text(rc: Int): String =
-    return_code_text.get(rc) match {
-      case None => ""
-      case Some(text) => " (" + text + ")"
+    private def text(rc: Int): String =
+    {
+      val txt =
+        rc match {
+          case `ok` => "OK"
+          case `error` => "ERROR"
+          case `failure` => "FAILURE"
+          case 127 => "COMMAND NOT FOUND"
+          case `interrupt` => "INTERRUPT"
+          case 131 => "QUIT SIGNAL"
+          case 137 => "KILL SIGNAL"
+          case 138 => "BUS ERROR"
+          case 139 => "SEGMENTATION VIOLATION"
+          case `timeout` => "TIMEOUT"
+          case 143 => "TERMINATION SIGNAL"
+          case _ => ""
+        }
+      if (txt.isEmpty) txt else " (" + txt + ")"
     }
 
-  val interrupt_rc = 130
-  val timeout_rc = 142
-
-  private val return_code_text =
-    Map(0 -> "OK",
-      1 -> "ERROR",
-      2 -> "FAILURE",
-      127 -> "COMMAND NOT FOUND",
-      interrupt_rc -> "INTERRUPT",
-      131 -> "QUIT SIGNAL",
-      137 -> "KILL SIGNAL",
-      138 -> "BUS ERROR",
-      139 -> "SEGMENTATION VIOLATION",
-      timeout_rc -> "TIMEOUT",
-      143 -> "TERMINATION SIGNAL")
+    def print_long(rc: Int): String = "Return code: " + rc + text(rc)
+    def print(rc: Int): String = "return code " + rc + text(rc)
+  }
 }
 
 final case class Process_Result(
@@ -50,13 +59,14 @@
   def error(err: String): Process_Result =
     if (err.isEmpty) this else errors(List(err))
 
-  def ok: Boolean = rc == 0
-  def interrupted: Boolean = rc == Process_Result.interrupt_rc
+  def ok: Boolean = rc == Process_Result.RC.ok
+  def interrupted: Boolean = rc == Process_Result.RC.interrupt
 
-  def timeout_rc: Process_Result = copy(rc = Process_Result.timeout_rc)
-  def timeout: Boolean = rc == Process_Result.timeout_rc
+  def timeout_rc: Process_Result = copy(rc = Process_Result.RC.timeout)
+  def timeout: Boolean = rc == Process_Result.RC.timeout
 
-  def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
+  def error_rc: Process_Result =
+    if (interrupted) this else copy(rc = rc max Process_Result.RC.error)
 
   def errors_rc(errs: List[String]): Process_Result =
     if (errs.isEmpty) this else errors(errs).error_rc
@@ -66,10 +76,10 @@
     else if (interrupted) throw Exn.Interrupt()
     else Exn.error(err)
 
-  def check: Process_Result = check_rc(_ == 0)
+  def check: Process_Result = check_rc(_ == Process_Result.RC.ok)
 
-  def print_return_code: String = Process_Result.print_return_code(rc)
-  def print_rc: String = Process_Result.print_rc(rc)
+  def print_return_code: String = Process_Result.RC.print_long(rc)
+  def print_rc: String = Process_Result.RC.print(rc)
 
   def print: Process_Result =
   {

--- a/src/Pure/Thy/export.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Thy/export.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -456,7 +456,7 @@
         progress.interrupt_handler {
           Build.build_logic(options, session_name, progress = progress, dirs = dirs)
         }
-      if (rc != 0) sys.exit(rc)
+      if (rc != Process_Result.RC.ok) sys.exit(rc)
     }
 
 

--- a/src/Pure/Tools/build.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Tools/build.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -147,8 +147,8 @@
     def info(name: String): Sessions.Info = results(name)._2
     val rc: Int =
       results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
-        foldLeft(0)(_ max _)
-    def ok: Boolean = rc == 0
+        foldLeft(Process_Result.RC.ok)(_ max _)
+    def ok: Boolean = rc == Process_Result.RC.ok
 
     override def toString: String = rc.toString
   }
@@ -286,7 +286,7 @@
       def ok: Boolean =
         process match {
           case None => false
-          case Some(res) => res.rc == 0
+          case Some(res) => res.ok
         }
     }
 
@@ -474,7 +474,7 @@
       }
     }
 
-    if (results.rc != 0 && (verbose || !no_build)) {
+    if (results.rc != Process_Result.RC.ok && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator
@@ -676,12 +676,12 @@
     val selection = Sessions.Selection.session(logic)
     val rc =
       if (!fresh && build(options, selection = selection,
-            build_heap = build_heap, no_build = true, dirs = dirs).ok) 0
+            build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, selection = selection, progress = progress,
           build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
       }
-    if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
+    if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc
   }
 }

--- a/src/Pure/Tools/build_job.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -145,7 +145,9 @@
             val msg = Symbol.output(unicode_symbols, cat_lines(errors))
             progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
           }
-          if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc))
+          if (rc != Process_Result.RC.ok) {
+            progress.echo("\n" + Process_Result.RC.print_long(rc))
+          }
       }
     })
   }
@@ -308,7 +310,7 @@
                   }
                 (rc, errors)
               }
-              catch { case ERROR(err) => (2, List(err)) }
+              catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
 
             session.protocol_command("Prover.stop", rc.toString)
             Build_Session_Errors(errors)
@@ -508,10 +510,10 @@
               errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                 errs.map(Protocol.Error_Message_Marker.apply))
           }
-          else if (progress.stopped && result.ok) result.copy(rc = Process_Result.interrupt_rc)
+          else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt)
           else result
         case Exn.Exn(Exn.Interrupt()) =>
-          if (result.ok) result.copy(rc = Process_Result.interrupt_rc)
+          if (result.ok) result.copy(rc = Process_Result.RC.interrupt)
           else result
         case Exn.Exn(exn) => throw exn
       }

--- a/src/Pure/Tools/server.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Tools/server.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -508,7 +508,7 @@
       }
       else if (operation_exit) {
         val ok = Server.exit(name)
-        sys.exit(if (ok) 0 else 2)
+        sys.exit(if (ok) Process_Result.RC.ok else Process_Result.RC.failure)
       }
       else {
         val log = Logger.make(log_file)

--- a/src/Pure/Tools/server_commands.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/Tools/server_commands.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -106,7 +106,7 @@
 
       if (results.ok) (results_json, results, options, base_info)
       else {
-        throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc),
+        throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc),
           results_json)
       }
     }

--- a/src/Tools/VSCode/src/language_server.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -345,7 +345,7 @@
   def exit(): Unit =
   {
     log("\n")
-    sys.exit(if (session_.value.isDefined) 2 else 0)
+    sys.exit(if (session_.value.isDefined) Process_Result.RC.failure else Process_Result.RC.ok)
   }
 
 

--- a/src/Tools/jEdit/src/main.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Tools/jEdit/src/main.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -133,7 +133,7 @@
           case exn: Throwable =>
             GUI.init_laf()
             GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
-            sys.exit(2)
+            sys.exit(Process_Result.RC.failure)
         }
       }
       start()

--- a/src/Tools/jEdit/src/session_build.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -172,9 +172,10 @@
             (Output.error_message_text(Exn.message(exn)) + "\n", Exn.failure_rc(exn))
         }
 
-      progress.echo(out + (if (rc == 0) "OK" else Process_Result.print_return_code(rc)) + "\n")
+      val ok = rc == Process_Result.RC.ok
+      progress.echo(out + (if (ok) "OK" else Process_Result.RC.print_long(rc)) + "\n")
 
-      if (rc == 0) JEdit_Sessions.session_start(options)
+      if (ok) JEdit_Sessions.session_start(options)
       else progress.echo("Session build failed -- prover process remains inactive!")
 
       return_code(rc)