public class GMFFConstants
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 |
GMFFConstants.ParseLocContext |
Constructor and Description |
---|
GMFFConstants() |
public static final java.lang.String DEFAULT_OUTPUT_FILE_NAME
public static final java.lang.String EXPORT_PARM_ON
public static final java.lang.String EXPORT_PARM_OFF
public static final java.lang.String CHARSET_ENCODING_ISO_8859
public static final java.lang.String EXPORT_TYPE_HTML
public static final java.lang.String EXPORT_TYPE_ALTHTML
public static final java.lang.String MODEL_A
public static final java.lang.String USER_EXPORT_CHOICE_ALL
public static final char FILE_TYPE_DOT
public static final java.lang.String METAMATH_DOLLAR_T_MESSAGE_DESCRIPTOR
public static final int METAMATH_DOLLAR_T_BUFFER_SIZE
public static final int METAMATH_DOLLAR_T_MAP_SIZE
public static final java.lang.String OPTION_VALUE_ALL
public static final java.lang.String PROOF_WORKSHEET_MESSAGE_DESCRIPTOR
public static final int PROOF_WORKSHEET_BUFFER_SIZE
public static final char APPEND_FILE_NAME_ERR_CHAR_1
public static final char APPEND_FILE_NAME_ERR_CHAR_2
public static final char APPEND_FILE_NAME_ERR_CHAR_3
public static final char OUTPUT_FILE_NAME_ERR_CHAR_1
public static final char OUTPUT_FILE_NAME_ERR_CHAR_2
public static final char OUTPUT_FILE_NAME_ERR_CHAR_3
public static final java.lang.String PRINT_TYPESETTING_DEFINITIONS
public static final java.lang.String RUNPARM_PRINT_OPTION
public static final GMFFUserExportChoice DEFAULT_USER_EXPORT_CHOICE
public static final java.lang.String DEFAULT_GMFF_HTML_DIRECTORY
public static final java.lang.String DEFAULT_GMFF_MODELS_HTML_DIRECTORY
public static final GMFFExportParms DEFAULT_EXPORT_PARMS_HTML
public static final java.lang.String DEFAULT_GMFF_ALTHTML_DIRECTORY
public static final java.lang.String DEFAULT_GMFF_MODELS_ALTHTML_DIRECTORY
public static final GMFFExportParms DEFAULT_EXPORT_PARMS_ALTHTML
public static final GMFFExportParms[] DEFAULT_EXPORT_PARMS
public static final EscapePair[] DEFAULT_ESCAPE_PAIRS
public static final GMFFUserTextEscapes GMFF_DEFAULT_USER_TEXT_ESCAPES_HTML
public static final GMFFUserTextEscapes GMFF_DEFAULT_USER_TEXT_ESCAPES_ALTHTML
public static final GMFFUserTextEscapes[] DEFAULT_USER_TEXT_ESCAPES
public static final int ESCAPE_PAIR_NUM_MIN
public static final int ESCAPE_PAIR_NUM_MAX
public static final int EXPORTER_MODEL_CACHE_INIT_SIZE
public static final java.lang.String MODEL_ERROR_MESSAGE_DESCRIPTOR
public static final int DEFAULT_MODEL_FILE_BUFFER_SIZE
public static final int EXPORT_BUFFER_DEFAULT_SIZE
public static final java.lang.String MODEL_A_FILE0_NAME
public static final java.lang.String MODEL_A_FILE2_NAME
public static final java.lang.String MODEL_A_STEP0_NAME
public static final java.lang.String MODEL_A_STEP1X_NAME
public static final java.lang.String MODEL_A_STEP2_NAME
public static final java.lang.String MODEL_A_STEP3X_NAME
public static final java.lang.String MODEL_A_STEP4_NAME
public static final java.lang.String MODEL_A_HEADER0_NAME
public static final java.lang.String MODEL_A_HEADER1X_NAME
public static final java.lang.String MODEL_A_HEADER2_NAME
public static final java.lang.String MODEL_A_HEADER3X_NAME
public static final java.lang.String MODEL_A_HEADER4_NAME
public static final java.lang.String MODEL_A_HEADER5X_NAME
public static final java.lang.String MODEL_A_HEADER6_NAME
public static final java.lang.String MODEL_A_HEADER7_NAME
public static final java.lang.String MODEL_A_COMMENT0_NAME
public static final java.lang.String MODEL_A_COMMENT1X_NAME
public static final java.lang.String MODEL_A_COMMENT2_NAME
public static final java.lang.String MODEL_A_DISTINCTVAR0_NAME
public static final java.lang.String MODEL_A_DISTINCTVAR1X_NAME
public static final java.lang.String MODEL_A_DISTINCTVAR2_NAME
public static final java.lang.String MODEL_A_DISTINCTVAR3X_NAME
public static final java.lang.String MODEL_A_DISTINCTVAR4_NAME
public static final java.lang.String MODEL_A_GENPROOF0_NAME
public static final java.lang.String MODEL_A_GENPROOF1X_NAME
public static final java.lang.String MODEL_A_GENPROOF2_NAME
public static final java.lang.String MODEL_A_FOOTER0_NAME
public static final ErrorCode ERRMSG_TOKENIZER_IO_ERROR
public static final ErrorCode ERRMSG_EMPTY_PROOF
public static final ErrorCode ERRMSG_BOGUS_LINE_1
public static final ErrorCode ERRMSG_LOAD_READLINE_IO_ERROR
public static final ErrorCode ERRMSG_WORK_STMT_LINE_START_ERROR
public static final ErrorCode ERRMSG_WORK_STMT_CONSTRUCTOR_ERROR
public static final ErrorCode ERRMSG_INVALID_LINE_LIST_ERROR
public static final ErrorCode ERRMSG_INVALID_HEADER_CONSTANTS_ERROR
public static final ErrorCode ERRMSG_INVALID_THEOREM_LABEL_ERROR
public static final ErrorCode ERRMSG_BUILD_EMPTY_OR_INVALID_WORKSHEET_ERROR
public static final ErrorCode ERRMSG_NO_EXPORT_TYPES_SELECTED_ERROR
public static final ErrorCode ERRMSG_INVALID_MODEL_ID_ERROR
public static final ErrorCode ERRMSG_EXPORT_PARMS_LIST_ERROR
public static final ErrorCode ERRMSG_USER_TEXT_ESCAPES_LIST_ERROR
public static final ErrorCode ERRMSG_INVALID_METAMATH_TYPESET_COMMENT_ERROR
public static final ErrorCode ERRMSG_NO_PROOF_FILES_SELECTED_ERROR
public static final ErrorCode ERRMSG_FILE_TYPE_BAD_MISSING
public static final ErrorCode ERRMSG_MAX_NBR_TO_EXPORT_BAD_MISSING
public static final ErrorCode ERRMSG_LABEL_OR_ASTERISK_BAD_MISSING
public static final ErrorCode ERRMSG_APPEND_FILE_NAME_ERROR
public static final ErrorCode ERRMSG_GMFF_THEOREM_EXPORT_PA_ERROR
public static final ErrorCode ERRMSG_NO_THEOREMS_SELECTED_ERROR
public static final ErrorCode INITIALIZATION_AUDIT_REPORT
public static final java.lang.String INITIALIZATION_AUDIT_REPORT_2
public static final java.lang.String INITIALIZATION_AUDIT_REPORT_3
public static final java.lang.String EXPORTER_AUDIT_REPORT
public static final ErrorCode ERRMSG_INPUT_DOLLAR_T_COMMENT_MM_FILE
public static final ErrorCode ERRMSG_TYPESET_DEF_NOT_FOUND_ERROR
public static final ErrorCode ERRMSG_MANDATORY_MODEL_NOT_FOUND_ERROR
public static final ErrorCode ERRMSG_EXPORT_CONFIRMATION
public static final ErrorCode ERRMSG_INPUT_FILE_EXISTS_NOT_A_FILE
public static final ErrorCode ERRMSG_INPUT_FILE_MISC_ERROR
public static final ErrorCode ERRMSG_GMFF_INPUT_FILE_NAME_BLANK
public static final ErrorCode ERRMSG_INPUT_FILE_NOT_FOUND
public static final ErrorCode ERRMSG_GMFF_FOLDER_NAME_BLANK
public static final ErrorCode ERRMSG_NOT_A_GMFF_FOLDER
public static final ErrorCode ERRMSG_GMFF_FOLDER_NOTFND
public static final ErrorCode ERRMSG_GMFF_FOLDER_MISC_ERROR
public static final ErrorCode ERRMSG_GMFF_FOLDER_READ_ERROR
public static final ErrorCode ERRMSG_GMFF_EXPORT_FILE_NAME_BLANK
public static final ErrorCode ERRMSG_EXPORT_FILE_EXISTS_NOT_A_FILE
public static final ErrorCode ERRMSG_EXPORT_FILE_EXISTS_CANNOT_UPDATE
public static final ErrorCode ERRMSG_EXPORT_FILE_MISC_ERROR
public static final ErrorCode ERRMSG_EXPORT_FILE_IO_ERROR
public static final ErrorCode ERRMSG_EXPORT_FILE_CHARSET_ERROR
public static final ErrorCode ERRMSG_GMFF_EXPORT_FILE_CHARSET_BLANK
public static final ErrorCode ERRMSG_PREMATURE_END_OF_DEF
public static final ErrorCode ERRMSG_MISSING_DOLLAR_T_TOKEN
public static final ErrorCode ERRMSG_NESTED_COMMENTS
public static final ErrorCode ERRMSG_MISSING_END_COMMENT
public static final ErrorCode ERRMSG_INVALID_KEYWORD_CHAR
public static final ErrorCode ERRMSG_KEYWORD_EMPTY_STRING
public static final ErrorCode ERRMSG_INVALID_SYM
public static final ErrorCode ERRMSG_AS_LITERAL_MISSING
public static final ErrorCode ERRMSG_MISSING_SEMICOLON
public static final ErrorCode ERRMSG_NOT_A_QUOTED_STRING
public static final ErrorCode ERRMSG_MISSING_END_DELIM
public static final ErrorCode ERRMSG_DUP_SYM_TYPESET_DEF
public static final ErrorCode ERRMSG_EXPORT_TYPE_BAD_MISSING
public static final ErrorCode ERRMSG_ON_OFF_BAD_MISSING
public static final ErrorCode ERRMSG_TYPESET_DEF_KEYWORD_BAD_MISSING
public static final ErrorCode ERRMSG_EXPORT_DIRECTORY_BAD_MISSING
public static final ErrorCode ERRMSG_EXPORT_DIRECTORY_BAD2
public static final ErrorCode ERRMSG_EXPORT_FILE_TYPE_BAD_MISSING
public static final ErrorCode ERRMSG_MODELS_DIRECTORY_BAD_MISSING
public static final ErrorCode ERRMSG_MODELS_DIRECTORY_BAD2
public static final ErrorCode ERRMSG_MODEL_ID_BAD_MISSING
public static final ErrorCode ERRMSG_CHARSET_ENCODING_BAD_MISSING
public static final ErrorCode ERRMSG_CHARSET_ENCODING_INVALID
public static final ErrorCode ERRMSG_CHARSET_ENCODING_UNSUPPORTED
public static final ErrorCode ERRMSG_OUTPUT_FILE_NAME_ERROR
public static final ErrorCode ERRMSG_ESCAPE_EXPORT_TYPE_BAD_MISSING
public static final ErrorCode ERRMSG_ESCAPE_PAIR_BAD2
public static final ErrorCode ERRMSG_ESCAPE_PAIR_NUM_BAD
public static final ErrorCode ERRMSG_ESCAPE_PAIR_REPLACEMENT_MISSING
public static final ErrorCode ERRMSG_USER_EXPORT_CHOICE_BAD_MISSING
public static final ErrorCode ERRMSG_TYPESET_DEFS_AUDIT
public static final java.lang.String ERRMSG_TYPESET_DEFS_AUDIT_2
public static final ErrorCode ERRMSG_GMFF_INITIALIZE_PARM_0_ERR
public static final ErrorCode ERRMSG_GMFF_PARSE_RUNPARM_PARM_4_ERR