public class MinProofWorksheet
extends java.lang.Object
MinProofWorksheet
is a minimalist ProofWorksheet
containing
just enough parsed proof data to generate a Model A type export file via
GMFF.
Initially, GMFF Model A (export type) is supported but additional Models
could be supported. Some Models might require the "Full Monte" -- our old
friend ProofWorksheet
, which requires full structural validation
edits for loading.
Constructor and Description |
---|
MinProofWorksheet(Messages messages)
Constructor for MinProofWorksheet.
|
Modifier and Type | Method and Description |
---|---|
int |
getLineCnt()
Returns the Proof Worksheet
lineCnt field. |
java.lang.String |
getLocAfter()
Returns the Proof Worksheet
locAfter field. |
java.util.List<MinProofWorkStmt> |
getMinProofWorkStmtList()
Returns the list of Proof Worksheet statements.
|
boolean |
getStructuralErrors()
Returns the Proof Worksheet
structuralErrors indicator. |
java.lang.String |
getTheoremLabel()
Returns the Proof Worksheet
theoremLabel field. |
void |
load(java.lang.String proofText)
Loads the Proof Worksheet text into the MinProofWorksheet.
|
void |
setLocAfter(java.lang.String s)
Sets the Proof Worksheet
locAfter field. |
void |
setStructuralErrors(boolean structuralErrors)
Sets the Proof Worksheet
structuralErrors indicator. |
void |
setTheoremLabel(java.lang.String s)
Sets the Proof Worksheet
theoremLabel field. |
void |
triggerBogusStmtLineStart(java.lang.String chunk,
int lineNbr) |
void |
triggerConstructorError(java.lang.Exception e,
int lineNbr) |
void |
triggerInvalidHeaderConstants(int lineNbr) |
void |
triggerInvalidTheoremLabel(java.lang.String theoremLabel,
int lineNbr) |
public MinProofWorksheet(Messages messages)
Builds an empty MinProofWorksheet marked as invalid so that it can be cached in ProofWorksheetCache regardless of its validity and successful loading.
messages
- The Messages
object.public void load(java.lang.String proofText)
proofText
- String data holding Proof Worksheet text.public java.util.List<MinProofWorkStmt> getMinProofWorkStmtList()
public boolean getStructuralErrors()
structuralErrors
indicator.public void setStructuralErrors(boolean structuralErrors)
structuralErrors
indicator.structuralErrors
- boolean indicator.public java.lang.String getTheoremLabel()
theoremLabel
field.public void setTheoremLabel(java.lang.String s)
theoremLabel
field.s
- Theorem Label field.public java.lang.String getLocAfter()
locAfter
field.public void setLocAfter(java.lang.String s)
locAfter
field.s
- locAfter field.public int getLineCnt()
lineCnt
field.public void triggerBogusStmtLineStart(java.lang.String chunk, int lineNbr)
public void triggerConstructorError(java.lang.Exception e, int lineNbr)
public void triggerInvalidTheoremLabel(java.lang.String theoremLabel, int lineNbr)
public void triggerInvalidHeaderConstants(int lineNbr)