public class MMJException
extends java.lang.Exception
ErrorCode
), which allows both for
efficient locating of the error by users or developers, as well as
customizable error suppression by type.
The primary difference between info messages and error messages is that an
info message generally throws this exception, while an info message will
merely create the exception object and pass it around. All of the message
output constructs work by creating members of this class at some point, and
produce messages headed by the error code, which has the format
X-YY-1234
.
Since this class extends Exception
, it is checked, as are all its
subclasses. In order to throw an unchecked exception, it is usually wrapped
in an IllegalStateException
or IllegalArgumentException
; the
first case is usually a programmer error, while the second might be more
generally used for validating input where checked exceptions are
inconvenient. In any case, the extract(Throwable)
class can be used
to get an embedded MMJException out of any exception.
Modifier and Type | Class and Description |
---|---|
static interface |
MMJException.ErrorContext
An error context is an extra piece of information about the location of
the error, such as "Theorem X" or "Line 2".
|
static class |
MMJException.FormatContext |
Modifier and Type | Field and Description |
---|---|
ErrorCode |
code |
java.util.List<MMJException.ErrorContext> |
ctxt |
Constructor and Description |
---|
MMJException(ErrorCode code,
java.lang.Object... args)
Constructor,
LangException with error message. |
MMJException(java.lang.Throwable cause,
ErrorCode code,
java.lang.Object... args)
Constructor,
LangException with error message and cause. |
Modifier and Type | Method and Description |
---|---|
MMJException |
addContext(MMJException.ErrorContext ec) |
static <T extends MMJException> |
addContext(MMJException.ErrorContext ec,
T e) |
protected void |
checkNS(java.lang.String ns) |
static MMJException |
extract(java.lang.Throwable t)
Gets an
MMJException in the cause of this throwable. |
<T extends MMJException.ErrorContext> |
getContext(java.lang.Class<T> clazz) |
java.lang.String |
getMessage() |
static boolean |
use(java.lang.Throwable t)
Returns true if this Throwable is not caused by the MMJ system, or the
MMJException cause has an enabled error code (see
ErrorCode.use() ); in the latter case the usage count for the
error is increased. |
public ErrorCode code
public java.util.List<MMJException.ErrorContext> ctxt
public MMJException(ErrorCode code, java.lang.Object... args)
LangException
with error message.code
- error message.args
- formatting arguments.public MMJException(java.lang.Throwable cause, ErrorCode code, java.lang.Object... args)
LangException
with error message and cause.cause
- The source exception, for stack tracingcode
- error message.args
- formatting arguments.public MMJException addContext(MMJException.ErrorContext ec)
public static <T extends MMJException> T addContext(MMJException.ErrorContext ec, T e)
public java.lang.String getMessage()
getMessage
in class java.lang.Throwable
public static MMJException extract(java.lang.Throwable t)
MMJException
in the cause of this throwable.t
- the throwablepublic static boolean use(java.lang.Throwable t)
MMJException
cause has an enabled error code (see
ErrorCode.use()
); in the latter case the usage count for the
error is increased.t
- the throwableprotected void checkNS(java.lang.String ns)
public <T extends MMJException.ErrorContext> T getContext(java.lang.Class<T> clazz)