public abstract class MinProofWorkStmt
extends java.lang.Object
Constructor and Description |
---|
MinProofWorkStmt(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinProofWorkStmt constructor.
|
Modifier and Type | Method and Description |
---|---|
abstract void |
buildModelAExport(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer)
Formats export data for the Proof Worksheet statement according to the
Model A specifications and loads the data into a specified
buffer. |
static MinProofWorkStmt |
constructStmt(MinProofWorksheet minProofWorksheet,
java.util.List<java.util.List<java.lang.String>> lineList)
constructStmt builds a MinProofWorkStmt from an List of
an List of String chunks which are either Metamath whitespace or Metamath
tokens. |
java.lang.String |
getCleanedLineString(int lineIndex)
Converts whitespace chunks in line of the
MinProofWorkStmt to
spaces. |
java.lang.String |
getCleanedLineString(int lineIndex,
int fromChunkIndex,
int toChunkIndex)
Converts whitespace chunks in part of a line of the
MinProofWorkStmt to spaces. |
protected boolean |
isChunkWhitespace(java.lang.String s) |
void |
typesetFormulaSymbols(GMFFExporter gmffExporter,
java.lang.StringBuilder exportBuffer,
java.lang.String[] lineChunks,
int startOfFormulaSymbols)
Utility function to typeset and reformat a portion of a
String
array containing Metamath tokens representing at least a portion of a
formula. |
public MinProofWorkStmt(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 static MinProofWorkStmt constructStmt(MinProofWorksheet minProofWorksheet, java.util.List<java.util.List<java.lang.String>> lineList)
constructStmt
builds a MinProofWorkStmt
from an List of
an List of String chunks which are either Metamath whitespace or Metamath
tokens.
The first line of a statement identifies the type of Proof Worksheet
statement. constructStmt
validates those simply in order to be
able to determine which type of Proof Worksheet statement must be
constructed. In addition it checks to see if the starting portion--up to
theorem label-- is valid, and then it extracts the theorem label and
stores it in the input minProofWorksheet object. Errors result in
accum'ing of error message(s) in the Messages
as well as setting
of structuralError
in the input MinProofWorksheet
object.
minProofWorksheet
- GMFF version of ProofWorksheet
lineList
- List of List of String chunks representing the text of a
ProofWorksheet
broken into Metamath whitespace and
tokens grouped by line of the ProofWorksheet
.MinProofWorkStmt
according to the first token of the
first line of the statement text.java.lang.IllegalArgumentException
- if lineList is empty or if the first
line has no String
chunks.public abstract void buildModelAExport(GMFFExporter gmffExporter, java.lang.StringBuilder exportBuffer) throws GMFFException
Model A
specifications and loads the data into a specified
buffer.
Export data is based on model files which vary according to the Model Id and Proof Worksheet statement type. In general, model files contain fragments of export data, such as html fragments -- but a model file may also represent a placeholder for insertion of formatted text from the Proof Worksheet. Model files are also categorized as Required or Optional. Required model files, if not found when read by the program trigger an error message and prevent export of the entire proof. Optional model files if not found when read simply prevent export of part of the proof -- for example, Comments -- and no error messages are generated. Placeholder model files, whether Required or Optional, which exist but contain no data indicate to the program that proof text is not to be output at this location in the export text.
Additional information may be found \GMFFDoc\GMFFModels.txt.
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 void typesetFormulaSymbols(GMFFExporter gmffExporter, java.lang.StringBuilder exportBuffer, java.lang.String[] lineChunks, int startOfFormulaSymbols)
String
array containing Metamath tokens representing at least a portion of a
formula.
There are two types of "chunks" to be typeset: whitespace chunks and non-whitespace chunks. Non-whitespace chunks are presumed to be Metamath ASCII symbols which are converted into export data (e.g. html) using the Metamath $t comment statement data. Whitespace chunks are cleaned so that they contain only spaces, and in addition, are shortened by one character for readability.
gmffExporter
- The GMFFExporter
requesting the export data
build.exportBuffer
- The StringBuilder
to which exported data is
to be output.lineChunks
- String
array containing Metamath tokens or
whitespace.startOfFormulaSymbols
- index into lineChunks
indicating the
beginning of the typesetting operation (which proceeds through
the end of the array -- effectively we are just bypassing an
initial part of the array.)public java.lang.String getCleanedLineString(int lineIndex)
MinProofWorkStmt
to
spaces.
By the time a Proof Worksheet statement gets to this part of the code, the only non-space whitespace character is Tab -- and on the Proof Assistant GUI Tab characters equate to one space. To be really safe, all whitespace chunk characters are converted to spaces.
lineIndex
- index of line in stmtLineChunks
to be "cleaned".public java.lang.String getCleanedLineString(int lineIndex, int fromChunkIndex, int toChunkIndex)
MinProofWorkStmt
to spaces.
By the time a Proof Worksheet statement gets to this part of the code, the only non-space whitespace character is Tab -- and on the Proof Assistant GUI Tab characters equate to one space. To be really safe, all whitespace chunk characters are converted to spaces.
lineIndex
- index of line in stmtLineChunks
to be "cleaned".fromChunkIndex
- index of first chunk in the line to be "cleaned".toChunkIndex
- exclusive endpoint (i.e. not thru) of chunk cleanup
operation :-)protected boolean isChunkWhitespace(java.lang.String s)