public class LangConstants
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.
Constructor and Description |
---|
LangConstants() |
public static final int SYM_TBL_INITIAL_SIZE_DEFAULT
The system will grow the table, as needed.
public static final int SYM_TBL_INITIAL_SIZE_MINIMUM
An arbitrary small number greater than zero :)
public static final int STMT_TBL_INITIAL_SIZE_DEFAULT
An arbitrary small number greater than zero :)
public static final int STMT_TBL_INITIAL_SIZE_MINIMUM
An arbitrary small number greater than zero :)
public static final ProofVerifier PROOF_VERIFIER_DEFAULT
The ProofVerifier can be added after the .mm file is loaded.
public static final SyntaxVerifier SYNTAX_VERIFIER_DEFAULT
The SyntaxVerifier can be added after the .mm file is loaded.
public static final int MAX_ERROR_MESSAGES_DEFAULT
The number of error messages is important, and is used to halt processing when the maximum is reached. Also, Proof Verification and/or Syntax Verification will not take place unless the .mm file was loaded with zero errors.
Set this number to 9999 if desired, it is not a problem unless you are short on memory.
public static final int MAX_INFO_MESSAGES_DEFAULT
There are not many info messages in mmj at this time. Basically they fall into the category of "warnings", but in the future might include audit or statistical data ("instrumentation").
public static final int SEQ_ASSIGNER_MIN_INTERVAL_SIZE
SEQ_ASSIGNER_MIN_INTERVAL_SIZE = 1.
public static final int SEQ_ASSIGNER_MAX_INTERVAL_SIZE
SEQ_ASSIGNER_MAX_INTERVAL_SIZE = 10000.
public static final int SEQ_ASSIGNER_INTERVAL_SIZE_DEFAULT
SEQ_ASSIGNER_INTERVAL_SIZE_DEFAULT = 1000.
public static final int SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_MIN
SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_MIN = 10.
public static final int SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_MAX
SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_MAX = 10000.
public static final int SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_DEFAULT
SEQ_ASSIGNER_INTERVAL_TBL_INITIAL_SIZE_DEFAULT = 100.
public static final int COMPRESS_LOW_BASE
public static final int COMPRESS_HIGH_BASE
public static final byte[] COMPRESS_LOW_DIGIT_CHARS
public static final byte[] COMPRESS_HIGH_DIGIT_CHARS
public static final byte COMPRESS_UNKNOWN_CHAR
public static final byte COMPRESS_REPEAT_CHAR
public static final byte COMPRESS_UNKNOWN_CHAR_VALUE
public static final byte COMPRESS_REPEAT_CHAR_VALUE
public static final byte COMPRESS_ERROR_CHAR_VALUE
public static final byte[] COMPRESS_VALID_CHARS
public static final int COMPRESS_OTHER_STMT_INIT_LEN
public static final int COMPRESS_REPEATED_SUBPROOF_INIT_LEN
public static final int COMPRESS_STEP_INIT_LEN
public static final int NBR_WORK_VARS_FOR_TYPE_MIN
public static final int NBR_WORK_VARS_FOR_TYPE_MAX
public static final int STARTING_WORK_VAR_SEQ_NBR_FOR_MOBJ
public static final java.lang.String WORK_VAR_DEFAULT_PREFIX
public static final int WORK_VAR_DEFAULT_NBR_FOR_TYP_CD
public static final int WV_OCCURS_IN_RENAME_LOOP
public static final int WV_OCCURS_IN_NOT_AT_ALL
public static final int WV_OCCURS_IN_ERROR
public static final boolean BOOK_MANAGER_ENABLED_DEFAULT
public static final int ALLOC_NBR_BOOK_CHAPTERS_INITIAL
If the number of input Chapters exceeds this value the ArrayList is automatically resized. As of August 2008 there were 33 Chapters in set.mm
public static final int ALLOC_NBR_BOOK_SECTIONS_INITIAL
If the number of input Sections exceeds this value the ArrayList is automatically resized. As of August 2008 there were about 1250 Sections in set.mm
public static final int SECTION_NBR_CATEGORIES
public static final int SECTION_SYM_CD
public static final int SECTION_VAR_HYP_CD
public static final int SECTION_SYNTAX_CD
public static final int SECTION_LOGIC_CD
public static final java.lang.String[] SECTION_DISPLAY_CAPTION
public static final java.lang.String CNST_SET_TYPE
public static final java.lang.String CHAPTER_TOSTRING_LITERAL
public static final java.lang.String SECTION_TOSTRING_LITERAL
public static final ErrorCode ERRMSG_MUST_DEF_CNST_AT_GLOBAL_LVL
public static final ErrorCode ERRMSG_CANNOT_END_GLOBAL_SCOPE
public static final ErrorCode ERRMSG_MISSING_END_SCOPE_AT_EOF
public static final ErrorCode ERRMSG_DJ_VARS_ARE_DUPS
public static final ErrorCode ERRMSG_STMT_TYP_UNDEF
public static final ErrorCode ERRMSG_STMT_TYP_NOT_DEF_AS_CNST
public static final ErrorCode ERRMSG_EXPR_SYM_NOT_DEF
public static final ErrorCode ERRMSG_EXPR_SYM_NOT_ACTIVE
public static final ErrorCode ERRMSG_EXPR_VAR_W_O_ACTIVE_VAR_HYP
public static final ErrorCode ERRMSG_DUP_STMT_LABEL
public static final ErrorCode ERRMSG_FORMULA_VAR_HYP_NOTFND
public static final ErrorCode ERRMSG_DUP_VAR_OR_CNST_SYM
public static final java.lang.String MISSING_PROOF_STEP
public static final ErrorCode ERRMSG_PROOF_HAS_NO_STEPS
public static final ErrorCode ERRMSG_PROOF_STEP_LABEL_NOTFND
public static final ErrorCode ERRMSG_FORWARD_PROOF_STEP_LABEL
public static final ErrorCode ERRMSG_PROOF_STEP_HYP_INACTIVE
public static final ErrorCode ERRMSG_VAR_IS_DUP_OF_CNST_SYM
public static final ErrorCode ERRMSG_VAR_IS_ALREADY_ACTIVE
public static final ErrorCode ERRMSG_STMT_VAR_UNDEF
public static final ErrorCode ERRMSG_STMT_VAR_NOT_DEF_AS_VAR
public static final ErrorCode ERRMSG_STMT_VAR_NOT_ACTIVE
public static final ErrorCode ERRMSG_MULT_ACTIVE_HYP_FOR_VAR
public static final ErrorCode ERRMSG_PARSED_RPN_INCOMPLETE
public static final ErrorCode ERRMSG_PARSED_RPN_EMPTY_STACK
public static final ErrorCode ERRMSG_PARSED_RPN_NOT_EMPTY_AT_END
public static final ErrorCode ERRMSG_MAX_ERROR_MSG_LT_1
public static final ErrorCode ERRMSG_MAX_INFO_MSG_LT_1
public static final ErrorCode ERRMSG_SYM_TBL_TOO_SMALL
public static final ErrorCode ERRMSG_STMT_TBL_TOO_SMALL
public static final ErrorCode ERRMSG_TREE_CONV_TO_RPN_FAILURE
public static final ErrorCode ERRMSG_RPN_CONV_TO_TREE_FAILURE
public static final ErrorCode ERRMSG_RPN_INVALID_NOT_ENOUGH_STMTS
public static final ErrorCode ERRMSG_STMT_LABEL_STRING_EMPTY
public static final java.lang.String DJVARS_LEFT_BRACKET
public static final java.lang.String DJVARS_RIGHT_BRACKET
public static final java.lang.String DJVARS_SEPARATOR
public static final ErrorCode ERRMSG_SYM_ID_STRING_EMPTY
public static final ErrorCode ERRMSG_TYP_CONV_DUP
public static final ErrorCode ERRMSG_ASSRT_SUBST_HYP_NOTFND
public static final ErrorCode ERRMSG_UNIFY_SUBST_HYP_NOTFND
public static final ErrorCode ERRMSG_SYM_ID_DUP_OF_STMT_LABEL
public static final ErrorCode ERRMSG_STMT_LABEL_DUP_OF_SYM_ID
public static final ErrorCode ERRMSG_SUBTREE_CONV_TO_RPN_FAILURE
public static final ErrorCode ERRMSG_DUP_SYM_MAP_PUT_ATTEMPT
public static final ErrorCode ERRMSG_DUP_STMT_MAP_PUT_ATTEMPT
public static final ErrorCode ERRMSG_THEOREM_LOADER_COMMIT_FAILED
public static final ErrorCode ERRMSG_COMPRESS_OTHER_NOTFND
public static final ErrorCode ERRMSG_COMPRESS_OTHER_BOGUS
public static final ErrorCode ERRMSG_COMPRESS_OTHER_VARHYP_POS
public static final ErrorCode ERRMSG_COMPRESS_NO_PROOF_BLOCKS
public static final ErrorCode ERRMSG_COMPRESS_PREMATURE_END
public static final ErrorCode ERRMSG_COMPRESS_NOT_ASCII
public static final ErrorCode ERRMSG_COMPRESS_BAD_CHAR
public static final ErrorCode ERRMSG_COMPRESS_BAD_UNK
public static final ErrorCode ERRMSG_COMPRESS_BAD_RPT
public static final ErrorCode ERRMSG_COMPRESS_BAD_RPT2
public static final ErrorCode ERRMSG_COMPRESS_BAD_RPT3
public static final ErrorCode ERRMSG_COMPRESS_CORRUPT
public static final ErrorCode ERRMSG_COMPRESS_OTHER_MAND
public static final ErrorCode ERRMSG_BAD_PARSE_STMT
public static final ErrorCode ERRMSG_TIMER_ID_NOTFND
public static final ErrorCode ERRMSG_TIMER_ID
public static final ErrorCode ERRMSG_DEFINE_WORK_VAR_TYPE_BAD
public static final ErrorCode ERRMSG_DEFINE_WORK_VAR_PREFIX_BAD
public static final ErrorCode ERRMSG_DEFINE_WORK_VAR_NBR_BAD
public static final ErrorCode ERRMSG_DEFINE_WORK_VAR_PFX_DUP
public static final ErrorCode ERRMSG_DEFINE_WORK_VAR_DUP
public static final ErrorCode ERRMSG_BOGUS_WORK_VAR_IN_ALLOC
public static final ErrorCode ERRMSG_TOO_FEW_WORK_VAR_FOR_TYP
public static final ErrorCode ERRMSG_VAR_IN_WORK_VAR_HYP
public static final ErrorCode ERRMSG_NULL_TARGET_VAR_HYP_PA_SUBST
public static final ErrorCode ERRMSG_INTERVAL_SIZE_RANGE_ERR
public static final ErrorCode ERRMSG_INTERVAL_TBL_SIZE_RANGE_ERR
public static final ErrorCode ERRMSG_SEQ_ASSIGNER_OUT_OF_NUMBERS
public static final ErrorCode ERRMSG_SEQ_ASSIGNER_ROLLBACK_STATE
public static final ErrorCode ERRMSG_SEQ_ASSIGNER_COMMIT_STATE
public static final ErrorCode ERRMSG_SEQ_ASSIGNER_ROLLBACK_AUDIT
public static final java.lang.String ERRMSG_THEOREM_CAPTION
public static final java.lang.String ERRMSG_LOGHYP_CAPTION
public static final java.lang.String ERRMSG_INSERTED_CAPTION
public static final java.lang.String ERRMSG_APPENDED_CAPTION
public static final ErrorCode ERRMSG_SEQ_ASSIGNER_CHECKPOINT_STATE
public static final ErrorCode ERRMSG_DJ_VARS_VARS_NOT_DEF_IN_EXT_FRAME
public static final ErrorCode ERRMSG_BM_UPDATE_W_MMT_SECTION_NOTFND
public static final ErrorCode ERRMSG_DUP_DJ_VARS_AFTER_CONSOLIDATION_ERR