--- 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")