public abstract class GMFFExporter
extends java.lang.Object
GMFFExporter
is the base class for creating export files.
There can be multiple Exporters in use at one time but the key is Export Type (e.g. "html", "althtml", etc.) and only one Exporter of a given Export Type can be active at one time.
The Export Type key is used to bring together and consolidate the various RunParm settings at GMFF initialization time.
What this all boils down to is that there cannot be two different Models in use for, say, Export Type "html" in a single execution of mmj2. However, the Export Type code is arbitrary and no functionality is hard-coded based on Export Type. So it is possible to define another Export Type such as "html2" which and use say, Model B, at the same time that Export Type "html" uses Model A -- you would just need to define all of the relevant parameters, including the Export Directory (so that the two exports don't overwrite each other.)
GMFFExporter
also contains a Map holding a cache of Model Files --
modelFileCacheMap
for the given Export Type. The purpose is to avoid
re-reading the model files over and over again.
GMFFExporter
also contains a number of utility functions which are
common to the different model exporters, such as ModelAExporter
,
which is an extension of GMFFExporter
.
Constructor and Description |
---|
GMFFExporter(GMFFManager gmffManager,
GMFFExportParms gmffExportParms,
GMFFUserTextEscapes gmffUserTextEscapes) |
Modifier and Type | Method and Description |
---|---|
void |
appendMandatoryModelFile(java.lang.StringBuilder exportBuffer,
java.lang.String mandatoryModelFileName,
java.lang.String theoremLabel)
Outputs the contents of a Mandatory Model File to the export buffer
throwing an exception if the file is not found.
|
void |
appendModelFileText(java.lang.StringBuilder exportBuffer,
java.lang.String modelFileText)
Appends text from a Model File to the output StringBuilder.
|
static GMFFExporter |
ConstructModelExporter(GMFFManager gmffManager,
GMFFExportParms gmffExportParms,
GMFFUserTextEscapes gmffUserTextEscapes)
A factory for generating GMFFExporters according to Model Id.
|
void |
escapeAndAppendProofText(java.lang.StringBuilder exportBuffer,
java.lang.String proofText)
Appends non-typeset text to the output buffer after escaping the text.
|
abstract GMFFException |
exportProofWorksheet(ProofWorksheetCache proofWorksheetCache,
java.lang.String appendFileName)
Abstract method to export a Proof Worksheet according to the pattern of a
Model.
|
java.lang.String |
getMandatoryModelFile(java.lang.String mandatoryModelFileName,
java.lang.String theoremLabel)
Returns a String containing the contents of a mandatory Model File.
|
Messages |
getMessages()
Get function to return the
Messages object. |
java.lang.String |
getOptionalModelFile(java.lang.String optionalModelFileName)
Returns a String containing the contents of an optional Model File.
|
protected void |
loadMinProofWorksheet(ProofWorksheetCache p)
Loads a
MinProofWorksheet object using the cached
proofText if the cache does not already contain a loaded instance
of the MinProofWorksheet . |
protected GMFFException |
outputToExportFile(java.lang.StringBuilder exportText,
java.lang.String appendFileName,
java.lang.String theoremLabel)
Writes the exported text to an output file.
|
java.lang.String |
readModelFile(java.lang.String modelFileName)
Returns the cached model file contents or if not cached already reads the
model file from disk and caches it.
|
void |
typesetAndAppendToken(java.lang.StringBuilder exportBuffer,
java.lang.String token,
java.lang.String theoremLabel)
If possible typesets the input token and outputs to the buffer.
|
protected java.lang.String |
writeExportFile(java.lang.String exportFileName,
java.lang.StringBuilder exportBuffer,
boolean append)
Writes the export text to the specified file and returns a String
containing the absolute path of the output file.
|
public GMFFExporter(GMFFManager gmffManager, GMFFExportParms gmffExportParms, GMFFUserTextEscapes gmffUserTextEscapes)
public static GMFFExporter ConstructModelExporter(GMFFManager gmffManager, GMFFExportParms gmffExportParms, GMFFUserTextEscapes gmffUserTextEscapes) throws GMFFException
Right now only Model A is defined, so this code looks peculiar.
Note: The Exporter's gmffExporterTypesetDefs
are loaded at
GMFFInitialize time, and are left null when the Exporter is initially
constructed.
gmffManager
- The GMFFManager
instance.gmffExportParms
- Export Parms for the output GMFFExporter
gmffUserTextEscapes
- Text Escapes for the output
GMFFExporter
GMFFExporter
GMFFException
- if an error occurredpublic abstract GMFFException exportProofWorksheet(ProofWorksheetCache proofWorksheetCache, java.lang.String appendFileName)
proofWorksheetCache
- ProofWorksheetCache
object containing
the proof to be exported.appendFileName
- File Name (minus File Type) of append file if the
regular file name is to be overridden (see documentation of
appendFileNames in GMFFDoc\GMFFRunParms.txt).null
if the export
failed (error messages are accumed in the Messages
object.)public Messages getMessages()
Messages
object.Messages
object.public void appendMandatoryModelFile(java.lang.StringBuilder exportBuffer, java.lang.String mandatoryModelFileName, java.lang.String theoremLabel) throws GMFFException
exportBuffer
- StringBuilder
containing the contents of the
export file.mandatoryModelFileName
- the File Name of the Model File within the
Models Directory for this Export Type.theoremLabel
- provided for use in error messages.GMFFException
- if other errors encountered (such as I/O errors.)public void appendModelFileText(java.lang.StringBuilder exportBuffer, java.lang.String modelFileText)
NOTE: does not escape the text because it is from a Model File and should already be escaped (as needed.)
exportBuffer
- StringBuilder
containing the contents of the
export file.modelFileText
- data from the Model File to be appended to the
exportBuffer.public void typesetAndAppendToken(java.lang.StringBuilder exportBuffer, java.lang.String token, java.lang.String theoremLabel)
Note: In the situation where the image file (.gif) referenced by the typesetting replacement text is not present in the Export Directory, some browsers display "ALT=" text. The Metamath set.mm $t statement uses the "ALT=" feature to display the ASCII token text. So in this scenario it may appear that the token was not found in the typesetting table, but the absence of an error message indicates that that is not the case.
exportBuffer
- StringBuilder
containing the contents of the
export file.token
- the Metamath token to be typeset.theoremLabel
- provided for use in error messages.public void escapeAndAppendProofText(java.lang.StringBuilder exportBuffer, java.lang.String proofText)
exportBuffer
- StringBuilder
containing the contents of the
export file.proofText
- output text from the proof worksheet to be escaped and
appended to the output buffer.public java.lang.String getMandatoryModelFile(java.lang.String mandatoryModelFileName, java.lang.String theoremLabel) throws GMFFException
Invokes the routine to read the Model File from the cache and if not
found -- because it is a Mandatory Model File -- throws the
GMFFMandatoryModelNotFoundException
exception.
mandatoryModelFileName
- the File Name of the Model File within the
Models Directory for this Export Type.theoremLabel
- provided for use in error messages.GMFFException
- if other errors encountered (such as I/O errors.)public java.lang.String getOptionalModelFile(java.lang.String optionalModelFileName) throws GMFFException
Invokes the routine to read the Model File from the cache and if not
found -- because it is an Optional Model File -- simply returns
null
.
optionalModelFileName
- the File Name of the Model File within the
Models Directory for this Export Type.GMFFException
- if an error occurredpublic java.lang.String readModelFile(java.lang.String modelFileName) throws GMFFException
Returns the file contents as a String, or throws an exception if not found.
modelFileName
- the File Name of the Model File within the Models
Directory for this Export Type.GMFFException
- if other errors encountered (such as I/O errors.)protected void loadMinProofWorksheet(ProofWorksheetCache p) throws GMFFException
MinProofWorksheet
object using the cached
proofText
if the cache does not already contain a loaded instance
of the MinProofWorksheet
.p
- the ProofWorksheetCache object.GMFFException
- if an error occurredprotected GMFFException outputToExportFile(java.lang.StringBuilder exportText, java.lang.String appendFileName, java.lang.String theoremLabel) throws GMFFException
Note: the name of the output file is generated here and it is a bit tricky. There is a hierarchy of possibilities:
appendFileName
is not null then that is the name used, and
the file is opened in "append mode", meaning the output is written to the
end of the file if the file already exists.
theoremLabel
is used as the file name.
Finally, to note, the output file name's File Type is appended to the file name computed above, in every case.
exportText
- the contents to be written out.appendFileName
- File Name (minus File Type) of append file if the
regular file name is to be overridden (see documentation of
appendFileNames in GMFFDoc\GMFFRunParms.txt).theoremLabel
- the label of the theorem whose proof is being
exported.GMFFException
- if the output operation fails.protected java.lang.String writeExportFile(java.lang.String exportFileName, java.lang.StringBuilder exportBuffer, boolean append) throws GMFFException
Note that here is where the last of the Export Parms come into play, including the Export Directory and the Charset Encoding name. Export Type is used in error messages, just to be helpful.
The actual I/O operation is handled by GMFFExportfile
.
exportFileName
- the output file, including file type.exportBuffer
- the output text data.append
- true if file is to be opened in "append mode", otherwise
false.GMFFException
- if the output operation fails.