public class Statementizer
extends java.lang.Object
implements java.io.Closeable
SrcStmt
.
(This is actually a somewhat inefficient intermediate step on the way to loading the source into memory, but is done this way to simplify the main code and to improve testability.)
Constructor and Description |
---|
Statementizer(Tokenizer t)
Construct a Statementizer from a Tokenizer.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
areLabelCharsValid(java.lang.String s)
Checks to see if each character in a String is a valid Metamath
character.
|
void |
bypassErrorStmt()
Attempts to bypass the current statement in the input Metamath file.
|
static int |
bypassNonWhitespace(java.lang.String s,
int i)
Bypasses Metamath non-whitespace in a String.
|
static int |
bypassWhitespace(java.lang.String s,
int i)
Bypasses Metamath whitespace in a String.
|
void |
close() |
java.lang.String |
getSourceId()
Returns the current Source information from the Tokenizer.
|
SrcStmt |
getStmt()
Return next MetaMath SrcStmt.
|
int |
getStmtNbr()
Return number of last statement parsed.
|
static java.lang.String |
getTitleIfApplicable(java.lang.String s,
java.lang.String idString)
Retrieves Chapter or Section title from a Comment String based on an
identifying pair of characters.
|
Tokenizer |
getTokenizer()
Returns the current Tokenizer.
|
static boolean |
isLabelOnProhibitedList(java.lang.String s)
Checks to see if a String is in the list of prohibited Metamath labels.
|
static boolean |
isValidLabel(java.lang.String s)
Checks to see if a String is a valid Metamath label name.
|
static boolean |
isValidMathSymbol(java.lang.String s)
Checks to see whether or not a String contains only symbols defined in
Metamath as valid math symbols.
|
void |
setStmtNbr(int s)
Sets statement number of the last statement parsed.
|
Tokenizer |
setTokenizer(Tokenizer t)
Switches the Tokenizer reader in use.
|
public Statementizer(Tokenizer t)
t
- input Tokenizer
stream.public static java.lang.String getTitleIfApplicable(java.lang.String s, java.lang.String idString)
s
- String containing Metamath Comment.idString
- identifying string of Chapter or Section title.public static int bypassWhitespace(java.lang.String s, int i)
s
- String containing Metamath characters.i
- index within String marking beginning of scan for whitespace.public static int bypassNonWhitespace(java.lang.String s, int i)
s
- String containing Metamath characters.i
- index within String marking beginning of scan for
non-whitespace.public static boolean isLabelOnProhibitedList(java.lang.String s)
See Metamath.pdf specification for the source list.
s
- String to check against the Prohibited Label list.public static boolean isValidLabel(java.lang.String s)
s
- String to checkpublic static boolean areLabelCharsValid(java.lang.String s)
See Metamath.pdf specification for the source list.
s
- String of characters to check for validity.public static boolean isValidMathSymbol(java.lang.String s)
s
- input token, should be pre-trimmed.public void close() throws java.io.IOException
close
in interface java.io.Closeable
close
in interface java.lang.AutoCloseable
java.io.IOException
public int getStmtNbr()
Statement number is simply a counter of the SrcStmt
processed so
far. It is not the same as mmj.lang.MObj.seq.
public void bypassErrorStmt() throws java.io.IOException
Bypass is intended to give the next next invocation of getStmt()
a good chance of finding a complete statement to parse, thus avoiding
multiple error messages caused by a single error.
java.io.IOException
- if I/O errorpublic void setStmtNbr(int s) throws java.lang.IllegalArgumentException
This may come in handy in conjunction with included files -- construct a
new Statementizer for the included file, set the stmtNbr, process, then
continue processing with the old Statementizer... after setting its
stmtNbr. Or...just use the setTokenizer
method to switch
Tokenizers! Easy.
s
- Metamath statement (sequence) number.java.lang.IllegalArgumentException
- if input statement number is less than
zero.public Tokenizer setTokenizer(Tokenizer t) throws java.lang.IllegalArgumentException
Intended for use with included MetaMath files ($[ xx.mm $]
command.)
t
- input Tokenizer
.java.lang.IllegalArgumentException
- if input Tokenizer is null.public java.lang.String getSourceId()
public Tokenizer getTokenizer()
public SrcStmt getStmt() throws MMIOException, java.io.IOException
SrcStmt
or null if EOF.java.io.IOException
- if I/O errorMMIOException
- if invalid SrcStmt read.