public class HeaderStmt extends ProofWorkStmt
Constructor and Description |
---|
HeaderStmt(ProofWorksheet w)
Default Constructor.
|
HeaderStmt(ProofWorksheet w,
java.lang.String theoremLabel,
java.lang.String locAfterLabel)
Constructor used for new proof.
|
Modifier and Type | Method and Description |
---|---|
int |
computeFieldIdCol(int fieldId)
Function used for cursor positioning.
|
java.lang.String |
load(java.lang.String firstToken)
load Header statement with Tokenizer input
|
boolean |
stmtIsIncomplete()
Is statement incomplete?
|
void |
tmffReformat()
Reformats Derivation Step using TMFF.
|
appendToProofText, getLineCnt, getProofWorksheet, getStmtDiagnosticInfo, getStmtText, hasMatchingRefLabel, hasMatchingStepNbr, loadAllStmtTextGetNextStmt, loadStmtTextGetNextStmt, loadStmtTextGetOptionalToken, loadStmtTextGetRequiredToken, setStmtCursorToCurrLineColumn, updateLineCntUsingTokenizer
public HeaderStmt(ProofWorksheet w)
w
- the owner ProofWorksheetpublic HeaderStmt(ProofWorksheet w, java.lang.String theoremLabel, java.lang.String locAfterLabel)
w
- the owner ProofWorksheettheoremLabel
- proof theorem labellocAfterLabel
- LOC_AFTER statement labelpublic boolean stmtIsIncomplete()
ProofWorkStmt
-- used primarily for cursor positioning:
-- a virtual method that checks the statement for the state of "incompleteness" of data as indicated by state variables in the specific ProofWorkStmt types.
stmtIsIncomplete
in class ProofWorkStmt
public int computeFieldIdCol(int fieldId)
computeFieldIdCol
in class ProofWorkStmt
fieldId
- value identify ProofWorkStmt field for cursor positioning,
as defined in PaConstants.FIELD_ID_*.public void tmffReformat()
tmffReformat
in class ProofWorkStmt
public java.lang.String load(java.lang.String firstToken) throws java.io.IOException, MMIOException, ProofAsstException
Output/Updates
- accum tokens and whitespace into stmtText,
checking for extra tokens or premature EOF
- throw exception if structural error found.
- set status to 0 if no errors
- return nextToken after trailing whitespace.
the start of the next statement.
- keep track of lineCnt, number of lines in
the statement.
- position cursor to field in error, as needed.
- Load Header statement fields.
load
in class ProofWorkStmt
firstToken
- first token of statementProofAsstException
- if validation error.java.io.IOException
- if IO errorMMIOException
- if an error occurred