public class ErrorCode
extends java.lang.Object
Each mmj message begins with a code, such as this:
E-LA-0007
where the format of the code is X-YY-9999
X
: error level
E
= Error
I
= Information
W
= Warning
A
= Abort (processing terminates, usually a bug).
YY
: source code
GM
= mmj.gmff package (see GMFFConstants
)
GR
= mmj.verify.Grammar and related code (see
GrammarConstants
)
IO
= mmj.mmio package (see MMIOConstants
)
LA
= mmj.lang package (see GMFFConstants
)
PA
= mmj.pa package (proof assistant) (see PaConstants
)
PR
= mmj.verify.VerifyProof and related code (see
ProofConstants
)
TL
= mmj.tl package (Theorem Loader).
TM
= mmj.tmff.AlignColumn and related code
UT
= mmj.util package. (see UtilConstants
)
TR
= mmj.transforms package (proof assistant) (see
TrConstants
)
9999
: sequential number within the source code, 0001 through
9999.
Modifier and Type | Class and Description |
---|---|
static class |
ErrorCode.ErrorLevel |
Modifier and Type | Field and Description |
---|---|
ErrorCode.ErrorLevel |
level |
java.lang.String |
messageRaw |
java.lang.String |
ns |
int |
number |
int |
usageCount |
int |
usageMax |
Constructor and Description |
---|
ErrorCode(java.lang.String code,
java.lang.String message) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
code() |
boolean |
enabled()
Similar to
use() , but does not increase the usage quota. |
static java.lang.String |
format(java.lang.String format,
java.lang.Object... args) |
static ErrorCode |
get(java.lang.String code) |
java.lang.String |
message(java.lang.Object... args) |
java.lang.String |
messageRaw(java.lang.Object... args) |
static ErrorCode |
of(java.lang.String combined) |
static ErrorCode |
of(java.lang.String code,
java.lang.String message) |
boolean |
use()
Increments this error code's usage count.
|
public final ErrorCode.ErrorLevel level
public final java.lang.String ns
public final int number
public final java.lang.String messageRaw
public int usageMax
public int usageCount
public java.lang.String code()
public java.lang.String messageRaw(java.lang.Object... args)
public java.lang.String message(java.lang.Object... args)
public boolean use()
public boolean enabled()
use()
, but does not increase the usage quota.public static java.lang.String format(java.lang.String format, java.lang.Object... args)
public static ErrorCode of(java.lang.String combined)
public static ErrorCode of(java.lang.String code, java.lang.String message)
public static ErrorCode get(java.lang.String code)