public class MMIOConstants
extends java.lang.Object
Contains gnasty 7-bit ASCII code-set dependencies! Gasp... I can't even begin to explain the ugliness of this bit-manipulating, symbol-tweaking horror show. Old school all the way :) Needs to be fixed to move into the 21st Century with Unicode -- that will be where we have 3D holo-IO infinite virtual blackboards and virtual reality gloves and voice recognition units that handle math symbols...in Phase IV of the project :)
From Metamath.pdf, 4.1:
The only characters that are allowed to appear in a Metamath source file are the 94 printable characters on standard ascii keyboards, which are digits, upper and lower case letters, and the following 32 special characters (plus the following non-printable (white space) characters: space, tab, carriage return, line feed, and form feed.:
` ~ ! @ # $ % ^ & * ( ) - _ = +
[ ] { } ; : ' " , . < > / ? \ |
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 |
MMIOConstants.FileContext |
static class |
MMIOConstants.LineColumnContext |
Constructor and Description |
---|
MMIOConstants() |
public static final int READER_BUFFER_SIZE
public static final byte PRINTABLE
WHITE_SPACE
characters.public static final byte WHITE_SPACE
public static final byte LABEL
'-', '_', '.'
.public static final byte MATH_SYMBOL
PRINTABLE
characters except
'$'
.public static final byte FILE_NAME
MATH_SYMBOL
.public static final byte[] VALID_CHAR_ARRAY
public static final java.util.Set<java.lang.String> PROHIBITED_LABELS
public static final char MM_KEYWORD_1ST_CHAR
public static final java.lang.String MM_CNST_KEYWORD
public static final java.lang.String MM_VAR_KEYWORD
public static final java.lang.String MM_DJ_VAR_KEYWORD
public static final java.lang.String MM_VAR_HYP_KEYWORD
public static final java.lang.String MM_LOG_HYP_KEYWORD
public static final java.lang.String MM_AXIOMATIC_ASSRT_KEYWORD
public static final java.lang.String MM_PROVABLE_ASSRT_KEYWORD
public static final java.lang.String MM_BEGIN_SCOPE_KEYWORD
public static final java.lang.String MM_END_SCOPE_KEYWORD
public static final java.lang.String MM_BEGIN_COMMENT_KEYWORD
public static final java.lang.String MM_END_COMMENT_KEYWORD
public static final char MM_BEGIN_COMPRESSED_PROOF_LIST_CHAR
public static final char MM_END_COMPRESSED_PROOF_LIST_CHAR
public static final char MM_END_STMT_KEYWORD_CHAR
public static final java.lang.String MM_BEGIN_FILE_KEYWORD
public static final java.lang.String MM_END_FILE_KEYWORD
public static final java.lang.String MM_END_STMT_KEYWORD
public static final java.lang.String MM_START_PROOF_KEYWORD
public static final java.lang.String MM_LABEL_IN_COMMENT_ESCAPE_STRING
public static final java.lang.String CHAPTER_ID_STRING
public static final java.lang.String SECTION_ID_STRING
public static final java.lang.String TYPESETTING_COMMENT_ID_STRING
public static final java.lang.String TYPESETTING_C_COMMENT_START
public static final java.lang.String TYPESETTING_C_COMMENT_END
public static final java.lang.String TYPESETTING_AS_LITERAL
public static final char TYPESETTING_SINGLE_QUOTE_CHAR
public static final char TYPESETTING_DOUBLE_QUOTE_CHAR
public static final char TYPESETTING_PLUS_CHAR
public static final char TYPESETTING_SLASH_CHAR
public static final char TYPESETTING_ASTERISK_CHAR
public static final char TYPESETTING_SEMICOLON_CHAR
public static final java.lang.String DEFAULT_TITLE
public static final boolean LOAD_COMMENTS_DEFAULT
If set to true then Metamath comments, at least on theorems, will be loaded into LogicalSystem.
If a Metamath comment statement immediately precedes a $p (Theorem) statement then the comment is stored on the mmj.lang.MObj in the "description" field. Later, perhaps, descriptions will be obtained for all MObj's, but for now we just need them for Proof Assistant.
public static final java.lang.String MISSING_PROOF_STEP
Equal "?". Every proof must have at least one step according to Metamath.pdf.
public static final boolean LOAD_PROOFS_DEFAULT
If set to true then Metamath proofs will be loaded as input. Otherwise, a single step = "?" will be passed to the SystemLoader when adding a Theorem.
public static final ErrorCode ERRMSG_SKIP_AHEAD_FAILED
public static final java.lang.String ERRMSG_TXT_LABEL
public static final java.lang.String ERRMSG_TXT_KEYWORD
public static final ErrorCode ERRMSG_INV_KEYWORD
public static final ErrorCode ERRMSG_EMPTY_CNST_STMT
public static final ErrorCode ERRMSG_INV_CHAR_IN_MATH_SYM
public static final ErrorCode ERRMSG_EMPTY_VAR_STMT
public static final ErrorCode ERRMSG_LESS_THAN_2_DJVARS
public static final ErrorCode ERRMSG_MISSING_LABEL
public static final ErrorCode ERRMSG_MISSING_START_COMMENT
public static final ErrorCode ERRMSG_INV_LABEL
public static final ErrorCode ERRMSG_EOF_AFTER_LABEL
public static final ErrorCode ERRMSG_MISSING_KEYWORD_AFTER_LABEL
public static final ErrorCode ERRMSG_MISLABELLED_KEYWORD
public static final ErrorCode ERRMSG_INV_COMMENT_CHAR_STR
public static final ErrorCode ERRMSG_INV_INCLUDE_FILE_NAME
public static final ErrorCode ERRMSG_PREMATURE_INCLUDE_STMT_EOF
public static final ErrorCode ERRMSG_STMT_HAS_DUP_TOKENS
public static final ErrorCode ERRMSG_STMT_PREMATURE_EOF
public static final ErrorCode ERRMSG_STMT_MISSING_TYPE
public static final ErrorCode ERRMSG_VAR_HYP_NE_2_TOKENS
public static final ErrorCode ERRMSG_PROOF_MISSING
public static final ErrorCode ERRMSG_INV_CHAR_IN_PROOF_STEP
public static final ErrorCode ERRMSG_PROOF_IS_EMPTY
public static final ErrorCode ERRMSG_SET_STMT_NBR_LT_0
public static final ErrorCode ERRMSG_SET_TOKENIZER_NULL
public static final ErrorCode ERRMSG_PREMATURE_COMMENT_EOF
public static final ErrorCode ERRMSG_COMPRESSED_PROOF_IS_EMPTY
public static final ErrorCode ERRMSG_INPUT_FILE_EMPTY
public static final ErrorCode ERRMSG_INCL_FILE_NOTFND
public static final ErrorCode ERRMSG_INCL_FILE_DUP
public static final ErrorCode ERRMSG_LOAD_REQ_FILE_DUP
public static final ErrorCode ERRMSG_LOAD_REQ_FILE_NOTFND
public static final ErrorCode ERRMSG_LOAD_MISC_IO
public static final MMJException.ErrorContext EOF_ERRMSG
public static final ErrorCode ERRMSG_INCLUDE_FILE_LIST_ERR
public static final ErrorCode ERRMSG_LOAD_LIMIT_STMT_NBR_REACHED
public static final ErrorCode ERRMSG_LOAD_LIMIT_STMT_LABEL_REACHED
public static final ErrorCode ERRMSG_INCLUDE_FILE_ARRAY_EMPTY