src/Tools/Setup/isabelle/setup/Exn.java
author wenzelm
Sat, 17 Jul 2021 13:42:21 +0200
changeset 74029 0701ff55780d
parent 73963 59b6f0462086
permissions -rw-r--r--
clarified build_props: empty module means no build; clarified signature; clarified errors;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73963
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/Setup/isabelle/setup/Exn.java
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     3
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     4
Support for exceptions (arbitrary throwables).
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     6
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle.setup;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     8
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
     9
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    10
import java.io.IOException;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    11
import java.util.LinkedList;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    12
import java.util.List;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    13
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    14
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    15
public class Exn
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    16
{
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    17
    /* interrupts */
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    18
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    19
    public static boolean is_interrupt(Throwable exn)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    20
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    21
        boolean found_interrupt = false;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    22
        Throwable e = exn;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    23
        while (!found_interrupt && e != null) {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    24
            found_interrupt = e instanceof InterruptedException;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    25
            e = e.getCause();
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    26
        }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    27
        return found_interrupt;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    28
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    29
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    30
    public static int INTERRUPT_RETURN_CODE = 130;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    31
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    32
    public static int return_code(Throwable exn, int rc)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    33
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    34
        return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    35
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    36
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    37
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    38
    /* message */
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    39
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    40
    public static String message(Throwable exn)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    41
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    42
        String msg = exn.getMessage();
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    43
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    44
        if (exn.getClass() == RuntimeException.class)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    45
        {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    46
            return msg == null || msg.isEmpty() ? "Error" : msg;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    47
        }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    48
        else if (exn instanceof IOException)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    49
        {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    50
            return msg == null || msg.isEmpty() ? "I/O error" : "I/O error: " + msg;
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    51
        }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    52
        else if (exn instanceof RuntimeException && !msg.isEmpty()) { return msg; }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    53
        else if (exn instanceof InterruptedException) { return "Interrupt"; }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    54
        else { return exn.toString(); }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    55
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    56
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    57
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    58
    /* print */
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    59
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    60
    public static String trace(Throwable exn)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    61
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    62
        List<String> list = new LinkedList<String>();
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    63
        for (StackTraceElement elem : exn.getStackTrace()) {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    64
            list.add(elem.toString());
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    65
        }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    66
        return Library.cat_lines(list);
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    67
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    68
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    69
    public static boolean debug()
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    70
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    71
        return System.getProperty("isabelle.debug", "").equals("true");
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    72
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    73
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    74
    public static String print(Throwable exn)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    75
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    76
        return debug() ? message(exn) + "\n" + trace(exn) : message(exn);
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    77
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    78
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    79
    public static String print_error(Throwable exn)
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    80
    {
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    81
        return Library.prefix_lines("*** ", print(exn));
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    82
    }
59b6f0462086 clarified modules;
wenzelm
parents:
diff changeset
    83
}