# HG changeset patch # User wenzelm # Date 1627297942 -7200 # Node ID 62e4ec8cff387dd40d67568a60e887996610e328 # Parent 0b1462ce5fda592914500c9734319f07e3de0ee8 clarified signature; diff -r 0b1462ce5fda -r 62e4ec8cff38 Admin/components/components.sha1 --- 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 diff -r 0b1462ce5fda -r 62e4ec8cff38 Admin/components/main --- 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 diff -r 0b1462ce5fda -r 62e4ec8cff38 src/Pure/General/exn.scala --- 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] = diff -r 0b1462ce5fda -r 62e4ec8cff38 src/Pure/System/command_line.scala --- 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) } diff -r 0b1462ce5fda -r 62e4ec8cff38 src/Tools/Setup/src/Exn.java --- 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; } diff -r 0b1462ce5fda -r 62e4ec8cff38 src/Tools/Setup/src/Setup.java --- 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)); } } } diff -r 0b1462ce5fda -r 62e4ec8cff38 src/Tools/jEdit/src/session_build.scala --- 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")