clarified modules;
authorwenzelm
Sun, 11 Jul 2021 16:57:30 +0200
changeset 74225 59b6f0462086
parent 74224 5351719ab2a0
child 74226 c9771e1b3223
clarified modules; clarified messages; clarified return code;
Admin/components/components.sha1
Admin/components/main
Admin/lib/Tools/build_setup
src/Pure/General/exn.scala
src/Pure/System/command_line.scala
src/Pure/library.scala
src/Tools/Setup/isabelle/setup/Environment.java
src/Tools/Setup/isabelle/setup/Exn.java
src/Tools/Setup/isabelle/setup/Library.java
src/Tools/Setup/isabelle/setup/Setup.java
--- 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));
         }
     }
 }