clarified signature;
authorwenzelm
Mon, 26 Jul 2021 13:12:22 +0200
changeset 74068 62e4ec8cff38
parent 74067 0b1462ce5fda
child 74069 ffbd1b7e5439
child 74070 a69a13c4b049
clarified signature;
Admin/components/components.sha1
Admin/components/main
src/Pure/General/exn.scala
src/Pure/System/command_line.scala
src/Tools/Setup/src/Exn.java
src/Tools/Setup/src/Setup.java
src/Tools/jEdit/src/session_build.scala
--- a/Admin/components/components.sha1	Mon Jul 26 13:04:55 2021 +0200
+++ b/Admin/components/components.sha1	Mon Jul 26 13:12:22 2021 +0200
@@ -135,6 +135,7 @@
 ac9739e38e4fbbfce1a71a0987a57b22f83922d3  isabelle_setup-20210724-1.tar.gz
 4554679cc8ea31e539655810a14d14216b383d0e  isabelle_setup-20210724-2.tar.gz
 127a75ae33e97480d352087fcb9b47a632d77169  isabelle_setup-20210724.tar.gz
+309909ec6d43ae460338e9af54c1b2a48adcb1ec  isabelle_setup-20210726.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56  jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39  jdk-11.0.2+9.tar.gz
--- a/Admin/components/main	Mon Jul 26 13:04:55 2021 +0200
+++ b/Admin/components/main	Mon Jul 26 13:12:22 2021 +0200
@@ -8,7 +8,7 @@
 flatlaf-1.2
 idea-icons-20210508
 isabelle_fonts-20210322
-isabelle_setup-20210724-2
+isabelle_setup-20210726
 jdk-15.0.2+7
 jedit-20210724
 jfreechart-1.5.1
--- a/src/Pure/General/exn.scala	Mon Jul 26 13:04:55 2021 +0200
+++ b/src/Pure/General/exn.scala	Mon Jul 26 13:12:22 2021 +0200
@@ -79,6 +79,9 @@
   def is_interrupt(exn: Throwable): Boolean =
     isabelle.setup.Exn.is_interrupt(exn)
 
+  def failure_rc(exn: Throwable): Int =
+    isabelle.setup.Exn.failure_rc(exn)
+
   def interruptible_capture[A](e: => A): Result[A] =
     try { Res(e) }
     catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
@@ -100,12 +103,6 @@
   }
 
 
-  /* POSIX return code */
-
-  def return_code(exn: Throwable, rc: Int): Int =
-    if (is_interrupt(exn)) Process_Result.interrupt_rc else rc
-
-
   /* message */
 
   def user_message(exn: Throwable): Option[String] =
--- a/src/Pure/System/command_line.scala	Mon Jul 26 13:04:55 2021 +0200
+++ b/src/Pure/System/command_line.scala	Mon Jul 26 13:12:22 2021 +0200
@@ -30,7 +30,7 @@
           catch {
             case exn: Throwable =>
               Output.error_message(Exn.print(exn))
-              Exn.return_code(exn, 2)
+              Exn.failure_rc(exn)
           }
         sys.exit(rc)
       }
--- a/src/Tools/Setup/src/Exn.java	Mon Jul 26 13:04:55 2021 +0200
+++ b/src/Tools/Setup/src/Exn.java	Mon Jul 26 13:12:22 2021 +0200
@@ -27,9 +27,9 @@
         return found_interrupt;
     }
 
-    public static int return_code(Throwable exn, int rc)
+    public static int failure_rc(Throwable exn)
     {
-        return is_interrupt(exn) ? 130 : rc;
+        return is_interrupt(exn) ? 130 : 2;
     }
 
 
--- a/src/Tools/Setup/src/Setup.java	Mon Jul 26 13:04:55 2021 +0200
+++ b/src/Tools/Setup/src/Setup.java	Mon Jul 26 13:12:22 2021 +0200
@@ -59,7 +59,7 @@
         }
         catch (Throwable exn) {
             echo_err(Exn.print_error(exn));
-            System.exit(Exn.return_code(exn, 2));
+            System.exit(Exn.failure_rc(exn));
         }
     }
 }
--- a/src/Tools/jEdit/src/session_build.scala	Mon Jul 26 13:04:55 2021 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Mon Jul 26 13:12:22 2021 +0200
@@ -169,7 +169,7 @@
         try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
         catch {
           case exn: Throwable =>
-            (Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
+            (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")