public class MinGeneratedProofStmt extends MinProofWorkStmt
MinProofWorksheet
.
Generated Proof statements are generated by mmj2 Proof Assistant when the user presses Ctrl-U (Unify) and unification successfully creates a Metamath proof -- which is simply a RPN (Reverse Polish Notation) list of Metamath statement labels. The Generated Proof statement consists of "$=" in column 1 of the first line of the Generated Proof statement followed by the space-separated list of statement labels.
Nothing is typeset by GMFF, and the labels are output as if they were just text, or comments (unlike the Metamath Proof Explorere web pages which contain hyperlinks for the statement labels.)
Constructor and Description |
---|
MinGeneratedProofStmt(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinGeneratedProofStmt constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
buildModelAExport(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer)
Formats export data for the Generated Proof statement according to the
Model A specifications and loads the data into a specified
buffer. |
constructStmt, getCleanedLineString, getCleanedLineString, isChunkWhitespace, typesetFormulaSymbols
public MinGeneratedProofStmt(MinProofWorksheet w, java.lang.String[][] slc)
w
- MinProofWorksheet
of which this statement is a part.slc
- Array of Array of String representing the lines and "chunks"
making up the MinProofWorkStmt
.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 MinGeneratedProofStmt
objects are
"optional", meaning that if any of the model files are not found, the
export process is continues normally but Generated Proof statements are
not output as part of the Proof Worksheet export.
Note the quirky handling of modelAGenProof1X
. If this model file
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.