--- a/Admin/components/components.sha1 Sun Jul 11 13:48:01 2021 +0200
+++ b/Admin/components/components.sha1 Sun Jul 11 16:57:30 2021 +0200
@@ -124,6 +124,7 @@
916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
+e413706694b0968245ee15183af2d464814ce0a4 isabelle_setup-20210711.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 Sun Jul 11 13:48:01 2021 +0200
+++ b/Admin/components/main Sun Jul 11 16:57:30 2021 +0200
@@ -8,7 +8,7 @@
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
-isabelle_setup-20210709
+isabelle_setup-20210711
jdk-15.0.2+7
jedit_build-20210708
jfreechart-1.5.1
--- a/Admin/lib/Tools/build_setup Sun Jul 11 13:48:01 2021 +0200
+++ b/Admin/lib/Tools/build_setup Sun Jul 11 16:57:30 2021 +0200
@@ -9,6 +9,8 @@
declare -a SOURCES=(
"Build.java"
"Environment.java"
+ "Exn.java"
+ "Library.java"
"Setup.java"
)
--- a/src/Pure/General/exn.scala Sun Jul 11 13:48:01 2021 +0200
+++ b/src/Pure/General/exn.scala Sun Jul 11 16:57:30 2021 +0200
@@ -77,15 +77,7 @@
/* interrupts */
def is_interrupt(exn: Throwable): Boolean =
- {
- var found_interrupt = false
- var e = exn
- while (!found_interrupt && e != null) {
- found_interrupt |= e.isInstanceOf[InterruptedException]
- e = e.getCause
- }
- found_interrupt
- }
+ isabelle.setup.Exn.is_interrupt(exn)
def interruptible_capture[A](e: => A): Result[A] =
try { Res(e) }
@@ -106,7 +98,7 @@
def expose(): Unit = if (Thread.interrupted()) throw apply()
def impose(): Unit = Thread.currentThread.interrupt()
- val return_code = 130
+ val return_code: Int = isabelle.setup.Exn.INTERRUPT_RETURN_CODE
}
@@ -139,8 +131,12 @@
user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
- /* trace */
+ /* print */
+
+ def debug(): Boolean = isabelle.setup.Exn.debug()
- def trace(exn: Throwable): String =
- exn.getStackTrace.mkString("\n")
+ def trace(exn: Throwable): String = isabelle.setup.Exn.trace(exn)
+
+ def print(exn: Throwable): String =
+ if (debug()) message(exn) + "\n" + trace(exn) else message(exn)
}
--- a/src/Pure/System/command_line.scala Sun Jul 11 13:48:01 2021 +0200
+++ b/src/Pure/System/command_line.scala Sun Jul 11 16:57:30 2021 +0200
@@ -21,8 +21,6 @@
def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
}
- var debug = false
-
def tool(body: => Unit): Unit =
{
val thread =
@@ -31,7 +29,7 @@
try { body; 0 }
catch {
case exn: Throwable =>
- Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else ""))
+ Output.error_message(Exn.print(exn))
Exn.return_code(exn, 2)
}
sys.exit(rc)
--- a/src/Pure/library.scala Sun Jul 11 13:48:01 2021 +0200
+++ b/src/Pure/library.scala Sun Jul 11 16:57:30 2021 +0200
@@ -105,7 +105,7 @@
def split_lines(str: String): List[String] = space_explode('\n', str)
def prefix_lines(prfx: String, str: String): String =
- if (str == "") str else cat_lines(split_lines(str).map(prfx + _))
+ isabelle.setup.Library.prefix_lines(prfx, str)
def indent_lines(n: Int, str: String): String =
prefix_lines(Symbol.spaces(n), str)
@@ -118,9 +118,7 @@
}
def trim_line(s: String): String =
- if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
- else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
- else s
+ isabelle.setup.Library.trim_line(s)
def trim_split_lines(s: String): List[String] =
split_lines(trim_line(s)).map(trim_line)
--- a/src/Tools/Setup/isabelle/setup/Environment.java Sun Jul 11 13:48:01 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Environment.java Sun Jul 11 16:57:30 2021 +0200
@@ -1,4 +1,4 @@
-/* Title: Pure/System/isabelle_env.scala
+/* Title: Tools/Setup/isabelle/setup/Environment.scala
Author: Makarius
Fundamental Isabelle system environment: quasi-static module with
@@ -212,8 +212,8 @@
Exec_Result(int rc, String out, String err)
{
_rc = rc;
- _out = out;
- _err = err;
+ _out = Library.trim_line(out);
+ _err = Library.trim_line(err);
}
public int rc() { return _rc; }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/isabelle/setup/Exn.java Sun Jul 11 16:57:30 2021 +0200
@@ -0,0 +1,83 @@
+/* Title: Tools/Setup/isabelle/setup/Exn.java
+ Author: Makarius
+
+Support for exceptions (arbitrary throwables).
+*/
+
+package isabelle.setup;
+
+
+import java.io.IOException;
+import java.util.LinkedList;
+import java.util.List;
+
+
+public class Exn
+{
+ /* interrupts */
+
+ public static boolean is_interrupt(Throwable exn)
+ {
+ boolean found_interrupt = false;
+ Throwable e = exn;
+ while (!found_interrupt && e != null) {
+ found_interrupt = e instanceof InterruptedException;
+ e = e.getCause();
+ }
+ 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;
+ }
+
+
+ /* message */
+
+ public static String message(Throwable exn)
+ {
+ String msg = exn.getMessage();
+
+ if (exn.getClass() == RuntimeException.class)
+ {
+ return msg == null || msg.isEmpty() ? "Error" : msg;
+ }
+ else if (exn instanceof IOException)
+ {
+ return msg == null || msg.isEmpty() ? "I/O error" : "I/O error: " + msg;
+ }
+ else if (exn instanceof RuntimeException && !msg.isEmpty()) { return msg; }
+ else if (exn instanceof InterruptedException) { return "Interrupt"; }
+ else { return exn.toString(); }
+ }
+
+
+ /* print */
+
+ public static String trace(Throwable exn)
+ {
+ List<String> list = new LinkedList<String>();
+ for (StackTraceElement elem : exn.getStackTrace()) {
+ list.add(elem.toString());
+ }
+ return Library.cat_lines(list);
+ }
+
+ public static boolean debug()
+ {
+ return System.getProperty("isabelle.debug", "").equals("true");
+ }
+
+ public static String print(Throwable exn)
+ {
+ return debug() ? message(exn) + "\n" + trace(exn) : message(exn);
+ }
+
+ public static String print_error(Throwable exn)
+ {
+ return Library.prefix_lines("*** ", print(exn));
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/isabelle/setup/Library.java Sun Jul 11 16:57:30 2021 +0200
@@ -0,0 +1,51 @@
+/* Title: Tools/Setup/isabelle/setup/Library.java
+ Author: Makarius
+
+Basic library.
+*/
+
+package isabelle.setup;
+
+
+import java.util.Arrays;
+import java.util.LinkedList;
+import java.util.List;
+
+
+public class Library
+{
+ public static String cat_lines(Iterable<? extends CharSequence> lines)
+ {
+ return String.join("\n", lines);
+ }
+
+ public static List<String> split_lines(String str)
+ {
+ if (str.isEmpty()) { return List.of(); }
+ else {
+ List<String> result = new LinkedList<String>();
+ result.addAll(Arrays.asList(str.split("\\n")));
+ return List.copyOf(result);
+ }
+ }
+
+ public static String prefix_lines(String prfx, String str)
+ {
+ if (str.isEmpty()) { return str; }
+ else {
+ StringBuilder result = new StringBuilder();
+ for (String s : split_lines(str)) {
+ result.append(prfx);
+ result.append(s);
+ }
+ return result.toString();
+ }
+ }
+
+ public static String trim_line(String s)
+ {
+ if (s.endsWith("\r\n")) { return s.substring(0, s.length() - 2); }
+ else if (s.endsWith("\r") || s.endsWith("\n")) { return s.substring(0, s.length() - 1); }
+ else { return s; }
+ }
+}
\ No newline at end of file
--- a/src/Tools/Setup/isabelle/setup/Setup.java Sun Jul 11 13:48:01 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Setup.java Sun Jul 11 16:57:30 2021 +0200
@@ -7,20 +7,19 @@
package isabelle.setup;
-import java.io.IOException;
-import java.security.NoSuchAlgorithmException;
-
-
class Setup
{
private static void echo(String msg)
{
System.out.println(msg);
-
+ }
+ private static void echo_err(String msg)
+ {
+ System.err.println(msg);
}
private static void fail(String msg)
{
- echo(msg);
+ echo_err(msg);
System.exit(2);
}
@@ -58,13 +57,9 @@
break;
}
}
- catch (InterruptedException e) {
- echo("Interrupt");
- System.exit(139);
- }
- catch (IOException | RuntimeException | NoSuchAlgorithmException e) {
- echo(e.getMessage());
- System.exit(1);
+ catch (Throwable exn) {
+ echo_err(Exn.print_error(exn));
+ System.exit(Exn.return_code(exn, 2));
}
}
}