public class MinHeaderStmt extends MinProofWorkStmt
MinProofWorksheet
.
The Header statement is vitally important even on a MinProofWorksheet
, which is validated only a minimal amount. The Header statement provides the
proof's theorem label which is used to construct the export file name. So, if
the Header is invalid the entire Proof Worksheet is updated with
structuralErrors = true
.
Constructor and Description |
---|
MinHeaderStmt(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinHeaderStmt constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
buildModelAExport(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer)
Formats export data for the Header statement according to the
Model A specifications and loads the data into a specified
buffer. |
boolean |
isTheoremLabelMinimallyValid()
Performs the minimal set of validation checks to ensure that the theorem
label can be used to generate a file name by the GMFF Extract process.
|
constructStmt, getCleanedLineString, getCleanedLineString, isChunkWhitespace, typesetFormulaSymbols
public MinHeaderStmt(MinProofWorksheet w, java.lang.String[][] slc)
The first line of the header is validated minimally.
$(THEOREM=
The validation/load code was extracted from
mmj.pa.HeaderStmt.load()
and
mmj.pa.HeaderStmt.validateTheoremLabel()
.
w
- the MinProofworksheet
object which contains the proof
step.slc
- Array of lines each comprised of an Array of String
s
called "chunks", which may be either Metamath whitespace or
Metamath tokens. Hence the acronym "slc" refers to Statement
Line Chunks.public void buildModelAExport(GMFFExporter gmffExporter, java.lang.StringBuilder exportBuffer) throws GMFFException
Model A
specifications and loads the data into a specified
buffer.
Model A model files for MinHeaderStmt
objects are "optional",
meaning that if any of the model files are not found, the export process
is continues normally but Header statements are not output as part of the
Proof Worksheet export.
Note the quirky handling of modelAHeader1X
,
modelAHeader3X
and modelAHeader5X
. If one of these model
files is empty then no data is output at that location. This quirky
feature will generally not be used but is provided for maximum
flexibility in creating export format models.
Additional information may be found \GMFFDoc\GMFFModels.txt.
buildModelAExport
in class MinProofWorkStmt
gmffExporter
- The GMFFExporter
requesting the export data
build.exportBuffer
- The StringBuilder
to which exported data is
to be output.GMFFException
- if errors are encountered during the export
process.public boolean isTheoremLabelMinimallyValid()
$(THEOREM=
The validation/load code was extracted from
mmj.pa.HeaderStmt.load()
and
mmj.pa.HeaderStmt.validateTheoremLabel()
.