public class TlConstants
extends java.lang.Object
There are two primary types of constants: parameters that are "hardcoded" which affect/control processing, and error/info messages.
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
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 |
TlConstants.DjVarsOption |
Constructor and Description |
---|
TlConstants() |
public static final java.lang.String SYNONYM_TRUE_1
public static final java.lang.String SYNONYM_TRUE_2
public static final java.lang.String SYNONYM_TRUE_3
public static final java.lang.String SYNONYM_FALSE_1
public static final java.lang.String SYNONYM_FALSE_2
public static final java.lang.String SYNONYM_FALSE_3
public static final java.lang.String FILE_SUFFIX_MMT
public static final int FILE_WRITER_BUFFER_SIZE
public static final int DEFAULT_DV_SRC_STMT_LIST_SIZE
public static final int DEFAULT_LOG_HYP_SRC_STMT_LIST_SIZE
public static final TlConstants.DjVarsOption THEOREM_LOADER_DJ_VARS_OPTION_DEFAULT
public static final boolean THEOREM_LOADER_AUDIT_MESSAGES_DEFAULT
public static final boolean THEOREM_LOADER_STORE_FORMULAS_ASIS_DEFAULT
public static final int THEOREM_LOADER_STORE_MM_INDENT_AMT_DEFAULT
public static final int THEOREM_LOADER_STORE_MM_INDENT_AMT_MIN
public static final int THEOREM_LOADER_STORE_MM_INDENT_AMT_MAX
public static final int THEOREM_LOADER_STORE_MM_RIGHT_COL_DEFAULT
public static final int THEOREM_LOADER_STORE_MM_RIGHT_COL_MIN
public static final int THEOREM_LOADER_STORE_MM_RIGHT_COL_MAX
public static final ErrorCode ERRMSG_MMT_FOLDER_NAME_BLANK
public static final ErrorCode ERRMSG_NOT_A_MMT_FOLDER
public static final ErrorCode ERRMSG_MMT_FOLDER_NOTFND
public static final ErrorCode ERRMSG_MMT_FOLDER_MISC_ERROR
public static final ErrorCode ERRMSG_MMT_FOLDER_UNSPECIFIED
public static final ErrorCode ERRMSG_MMT_FOLDER_READ_ERROR
public static final ErrorCode ERRMSG_MMT_FOLDER_FILE_NULL
public static final ErrorCode ERRMSG_MMT_THEOREM_LABEL_BLANK
public static final ErrorCode ERRMSG_MMT_THEOREM_NOT_A_FILE
public static final ErrorCode ERRMSG_MMT_THEOREM_NOTFND
public static final ErrorCode ERRMSG_MMT_THEOREM_FILE_MISC_ERROR
public static final ErrorCode ERRMSG_MMT_THEOREM_FILE_NOTFND
public static final ErrorCode ERRMSG_MMT_THEOREM_FILE_TYPE_BOGUS
public static final ErrorCode ERRMSG_MMT_THEOREM_WRITE_IO_ERROR
public static final ErrorCode ERRMSG_MMT_THEOREM_CLOSE_IO_ERROR
public static final ErrorCode ERRMSG_MMT_THEOREM_FILE_IO_ERROR
public static final ErrorCode ERRMSG_MMT_THEOREM_FILE_BAD_KEYWORD
public static final ErrorCode ERRMSG_BEGIN_SCOPE_MUST_BE_FIRST
public static final ErrorCode ERRMSG_END_SCOPE_MUST_BE_LAST
public static final ErrorCode ERRMSG_BEGIN_SCOPE_MISSING
public static final ErrorCode ERRMSG_EXTRA_THEOREM_STMT
public static final ErrorCode ERRMSG_THEOREM_LABEL_MISMATCH
public static final ErrorCode ERRMSG_THEOREM_LABEL_HYP_DUP
public static final ErrorCode ERRMSG_THEOREM_FILE_THEOREM_MISSING
public static final ErrorCode ERRMSG_THEOREM_LOG_HYP_SEQ_ERR
public static final ErrorCode ERRMSG_THEOREM_DV_SEQ_ERR
public static final ErrorCode ERRMSG_LOG_HYP_LABEL_HYP_DUP
public static final ErrorCode ERRMSG_END_SCOPE_MISSING
public static final ErrorCode ERRMSG_BEGIN_END_SCOPE_PAIR_MISSING
public static final ErrorCode ERRMSG_MMT_THEOREM_FILE_BOGUS_KEYWORD
public static final ErrorCode ERRMSG_SRC_STMT_SYM_NOTFND
public static final ErrorCode ERRMSG_LOG_HYP_STMT_MISMATCH
public static final ErrorCode ERRMSG_LOG_HYP_FORMULA_MISMATCH
public static final ErrorCode ERRMSG_THEOREM_PROOF_COMPRESSED
public static final ErrorCode ERRMSG_THEOREM_STMT_MISMATCH
public static final ErrorCode ERRMSG_THEOREM_FORMULA_MISMATCH
public static final ErrorCode ERRMSG_PROOF_LABEL_ERR
public static final ErrorCode ERRMSG_LOG_HYPS_DONT_MATCH
public static final ErrorCode ERRMSG_USED_THEOREM_SEQ_TOO_HIGH
public static final ErrorCode ERRMSG_PROOF_LABEL_SEQ_TOO_HIGH
public static final ErrorCode ERRMSG_MMT_STMT_PARSE_ERR
public static final ErrorCode ERRMSG_NEW_THEOREM_OLD_LOG_HYP
public static final ErrorCode ERRMSG_DJ_VAR_SYM_NOT_A_VAR
public static final ErrorCode ERRMSG_HYP_ADDED_TWICE_ERR
public static final ErrorCode ERRMSG_MMT_TYP_CD_NOT_VALID
public static final ErrorCode ERRMSG_AUDIT_MSG_THEOREM_ADD
public static final ErrorCode ERRMSG_AUDIT_MSG_THEOREM_UPD
public static final ErrorCode ERRMSG_DUP_MMT_THEOREM
public static final ErrorCode ERRMSG_ROLLBACK
public static final ErrorCode ERRMSG_CYCLIC_REF_ERROR
public static final ErrorCode ERRMSG_ROLLBACK_FAILED
public static final ErrorCode ERRMSG_INVALID_DJ_VARS_OPTION
public static final ErrorCode ERRMSG_INVALID_BOOLEAN
public static final ErrorCode ERRMSG_EXPORT_FORMAT_PROOF_WORKSHEET_ERR
public static final ErrorCode ERRMSG_HYP_MISSING_FOR_EXPORTED_PROOF_WORKSHEET
public static final ErrorCode ERRMSG_THEOREM_LOADER_TEXT_UNIFY_ERROR
public static final ErrorCode ERRMSG_STORE_IN_LOG_SYS_AND_MMT_FOLDER_OK
public static final ErrorCode ERRMSG_STORE_IN_MMT_FOLDER_OK