public class MinProofStepStmt extends MinProofWorkStmt
The term "proof step" in Proof Worksheet terminology is any Proof Worksheet
statement that contains a formula -- these are MinHypothesisStep
and
MinDerivationStep
, the latter includes the final step, the "qed"
step.
Constructor and Description |
---|
MinProofStepStmt(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinProofStepStmt constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
buildModelAExport(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer)
Formats export data for the proof step statement according to the
Model A specifications and loads the data into a specified
buffer. |
constructStmt, getCleanedLineString, getCleanedLineString, isChunkWhitespace, typesetFormulaSymbols
public MinProofStepStmt(MinProofWorksheet w, java.lang.String[][] slc)
w
- the MinProofworksheet
object which contains the proof
step.slc
- Array of proof step 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 MinProofStepStmt
objects are "mandatory",
meaning that if any of the model files are not found, the export process
is halted and an error message is generated.
Export of a proof step involves formatting two things: the part of each line prior to the first formula symbol on that line, and the typesetting and formatting of each formula symbol.
We go to a lot of trouble to format the pre-formula part of the line because it is vital to preserve the indentation before the formula symbols -- even though the process of generating typeset formulas will necessarily alter the indentations of the formula's symbols.
Note the quirky handling of modelAStep1X
and modelAStep3X
. 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.