# HG changeset patch
# User wenzelm
# Date 1627297495 -7200
# Node ID 0b1462ce5fda592914500c9734319f07e3de0ee8
# Parent  b3f072aa46908434897258334938f686f6e7eeaa
clarified signature;

diff -r b3f072aa4690 -r 0b1462ce5fda src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Pure/General/exn.scala	Mon Jul 26 13:04:55 2021 +0200
@@ -97,15 +97,13 @@
     def dispose(): Unit = Thread.interrupted()
     def expose(): Unit = if (Thread.interrupted()) throw apply()
     def impose(): Unit = Thread.currentThread.interrupt()
-
-    val return_code: Int = isabelle.setup.Exn.INTERRUPT_RETURN_CODE
   }
 
 
   /* POSIX return code */
 
   def return_code(exn: Throwable, rc: Int): Int =
-    if (is_interrupt(exn)) Interrupt.return_code else rc
+    if (is_interrupt(exn)) Process_Result.interrupt_rc else rc
 
 
   /* message */
diff -r b3f072aa4690 -r 0b1462ce5fda src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Pure/General/ssh.scala	Mon Jul 26 13:04:55 2021 +0200
@@ -302,10 +302,10 @@
 
       val rc =
         try { exit_status.join }
-        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+        catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
 
       close()
-      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+      if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)
     }
diff -r b3f072aa4690 -r 0b1462ce5fda src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Pure/System/bash.scala	Mon Jul 26 13:04:55 2021 +0200
@@ -219,11 +219,11 @@
 
       val rc =
         try { join }
-        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
+        catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
 
       watchdog_thread.foreach(_.cancel())
 
-      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+      if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
@@ -246,7 +246,7 @@
 
       val is_interrupt =
         result match {
-          case Exn.Res(res) => res.rc == Exn.Interrupt.return_code
+          case Exn.Res(res) => res.rc == Process_Result.interrupt_rc
           case Exn.Exn(exn) => Exn.is_interrupt(exn)
         }
 
diff -r b3f072aa4690 -r 0b1462ce5fda src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Pure/System/process_result.scala	Mon Jul 26 13:04:55 2021 +0200
@@ -16,20 +16,22 @@
       case None => ""
       case Some(text) => " (" + text + ")"
     }
+
+  val interrupt_rc = 130
+  val timeout_rc = 142
+
   private val return_code_text =
     Map(0 -> "OK",
       1 -> "ERROR",
       2 -> "FAILURE",
       127 -> "COMMAND NOT FOUND",
-      130 -> "INTERRUPT",
+      interrupt_rc -> "INTERRUPT",
       131 -> "QUIT SIGNAL",
       137 -> "KILL SIGNAL",
       138 -> "BUS ERROR",
       139 -> "SEGMENTATION VIOLATION",
-      142 -> "TIMEOUT",
+      timeout_rc -> "TIMEOUT",
       143 -> "TERMINATION SIGNAL")
-
-  val timeout_rc = 142
 }
 
 final case class Process_Result(
@@ -49,7 +51,7 @@
     if (err.isEmpty) this else errors(List(err))
 
   def ok: Boolean = rc == 0
-  def interrupted: Boolean = rc == Exn.Interrupt.return_code
+  def interrupted: Boolean = rc == Process_Result.interrupt_rc
 
   def timeout_rc: Process_Result = copy(rc = Process_Result.timeout_rc)
   def timeout: Boolean = rc == Process_Result.timeout_rc
diff -r b3f072aa4690 -r 0b1462ce5fda src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Mon Jul 26 13:04:55 2021 +0200
@@ -503,7 +503,7 @@
                 errs.map(Protocol.Error_Message_Marker.apply))
           }
         case Exn.Exn(Exn.Interrupt()) =>
-          if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
+          if (result.ok) result.copy(rc = Process_Result.interrupt_rc) else result
         case Exn.Exn(exn) => throw exn
       }
     }
diff -r b3f072aa4690 -r 0b1462ce5fda src/Tools/Setup/src/Exn.java
--- a/src/Tools/Setup/src/Exn.java	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Tools/Setup/src/Exn.java	Mon Jul 26 13:04:55 2021 +0200
@@ -27,11 +27,9 @@
         return found_interrupt;
     }
 
-    public static int INTERRUPT_RETURN_CODE = 130;
-
     public static int return_code(Throwable exn, int rc)
     {
-        return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
+        return is_interrupt(exn) ? 130 : rc;
     }