public class MinDistinctVariablesStmt extends MinProofWorkStmt
A Distinct Variables statement consists of a "$d" in column one of the first line of the statemenet followed by a list of variables. Model A provides for typesetting of the variables as well as maintaining indentation prior to the first variable.
Constructor and Description |
---|
MinDistinctVariablesStmt(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinDistinctVariablesStmt constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
buildModelAExport(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer)
Formats export data for the Distinct Variables statement according to the
Model A specifications and loads the data into a specified
buffer. |
constructStmt, getCleanedLineString, getCleanedLineString, isChunkWhitespace, typesetFormulaSymbols
public MinDistinctVariablesStmt(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 MinDistinctVariablesStmt
objects are
"optional", meaning that if any of the model files are not found, the
export process is continues normally but Distinct Variables statements
are not output as part of the Proof Worksheet export.
Export of a Distinct Variables statement involves formatting two things: the part of each line prior to the first variable symbol on that line, and the typesetting and formatting of variable symbol.
We go to a lot of trouble to format the pre-variable part of the line because it is important to preserve the indentation -- even though the process of generating typeset symbols necessarily alters the indentations of the individual symbols.
Note the quirky handling of modelADistinctVar1X
and
modelADistinctVar3X
. 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.