public class MinCommentStmt extends MinProofWorkStmt
MinProofWorksheet
.
Proof Worksheet Comment statements consist of just an "*" in column one of the first line of the statement followed by text characters -- which must be valid Metamath characters but are not otherwise validated.
GMFF typesets nothing on the Comment statement, everything is output as just "escaped" text.
Constructor and Description |
---|
MinCommentStmt(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinCommentStmt constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
buildModelAExport(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer)
Formats export data for the Comment statement according to the
Model A specifications and loads the data into a specified
buffer. |
constructStmt, getCleanedLineString, getCleanedLineString, isChunkWhitespace, typesetFormulaSymbols
public MinCommentStmt(MinProofWorksheet w, java.lang.String[][] slc)
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 MinCommentStmt
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 modelAGenComment1X
. 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.