public class GMFFManager
extends java.lang.Object
One thing that is different about GMFFManager
than other "manager"
type classes in mmj2 is that the GMFFManager
object is instantiated
by the LogicalSystemBoss
in the util
package rather than the
GMFFBoss
. This is because Metamath $t Comment statement(s) are
accumulated during the LoadFile
process -- though not parsed at that
time. Hence, a reference to the GMFFManager
instance is stored in
LogicalSystem
.
Another thing that is different than typical mmj2 processing is that the GMFF
RunParms which establish settings for parameters are not validated when the
RunParms are initially read. Nothing in GMFF happens until the first time the
user -- or a command-style GMFF RunParm -- requests that GMFF typeset
something. This functionality matches the way Metamath works and also saves
users who have no interest in using GMFF from aggravation if there are errors
in the GMFF-related inputs. A side-effect of delayed validation of GMFF
RunParms is additional complexity. GMFFManager
deals with that
complexity in initialization()
where all of the cached RunParms are
validated and merged with default settings for parameters.
Constructor and Description |
---|
GMFFManager(java.io.File filePath,
Messages messages)
Standard constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
accumInputGMFFExportParms(GMFFExportParms inputGMFFExportParms)
Caches parameters from one RunParm for later validation and use.
|
void |
accumInputGMFFUserTextEscapesList(GMFFUserTextEscapes inputGMFFUserTextEscapes)
Caches parameters from one RunParm for later validation and use.
|
void |
cacheTypesettingCommentForGMFF(java.lang.String comment)
Caches one Metamath $t Comment statement for later validation and use.
|
void |
exportFromFolder(java.lang.String inputDirectory,
java.lang.String theoremLabelOrAsterisk,
java.lang.String inputFileType,
java.lang.String maxNumberToExport,
java.lang.String appendFileNameIn)
Exports one or a range of Proof Worksheets of a given file type from a
designated directory.
|
java.util.List<GMFFException> |
exportProofWorksheet(java.lang.String proofText,
java.lang.String appendFileName)
Exports a single Proof Worksheet to files in the requested formats.
|
void |
exportTheorem(java.lang.String theoremLabelOrAsterisk,
java.lang.String maxNumberToExport,
java.lang.String appendFileNameIn,
ProofAsst proofAsst)
Exports one theorem or a range of theorems from
LogicalSystem . |
void |
forceReinitialization()
Forces GMFF to re-initialize itself the next time a service request is
received by settting
gmffInitialized to false . |
void |
generateInitializationAuditReport()
Generates and outputs to the Messages object an audit report of the final
results of GMFF initialization showing the parameters and settings in
use.
|
void |
generateTypesettingDefinitionsReport()
Generates and outputs to the Messages object an audit report of the
Metamath $t typesetting definitions after parsing of the input Metamath
file.
|
Messages |
getMessages()
Gets the
messages object. |
java.util.Map<java.lang.String,Sym> |
getSymTbl()
Gets the
symTbl for use in generating GMFF exports. |
void |
gmffExportOneTheorem(java.lang.String theoremLabel,
java.lang.String appendFileName,
ProofAsst proofAsst)
Exports one
Theorem from the LogicalSystem . |
void |
gmffExportOneTheorem(Theorem theorem,
java.lang.String appendFileName,
ProofAsst proofAsst)
Exports one
Theorem from the LogicalSystem . |
void |
gmffInitialize(boolean printTypesettingDefinitions)
Calls
initialize() , generates an audit report of GMFF RunParms
and default settings,mand if requested, prints the typesetting
definitions obtained from the input Metamath file(s) $t Comment
statements. |
boolean |
isGMFFInitialized()
Returns the
gmffInitialized boolean variable. |
void |
parseMetamathTypesetComment(java.lang.String typesetDefKeyword,
java.lang.String myDirectory,
java.lang.String myMetamathTypesetCommentFileName,
boolean runParmPrintOption)
Implements RunParm GMFFParseMMTypesetDefsComment.
|
void |
setInputGMFFUserExportChoice(GMFFUserExportChoice choice)
Stores the contents of the
GMFFUserExportChoice from one RunParm
for later validation and use. |
void |
setSymTbl(java.util.Map<java.lang.String,Sym> symTbl)
Sets the
symTbl for use in generating GMFF exports. |
public GMFFManager(java.io.File filePath, Messages messages)
Called by LogicalSystemBoss
when the first LoadFile
RunParm is executed.
Sets up GMFF data structures but does not load them. Sets
gmffInitialized
to false
to trigger initialization when
the first GMFF service request is received.
filePath
- path for building directories.messages
- The Messages object.public void gmffInitialize(boolean printTypesettingDefinitions) throws GMFFException
initialize()
, generates an audit report of GMFF RunParms
and default settings,mand if requested, prints the typesetting
definitions obtained from the input Metamath file(s) $t Comment
statements.
This function is called by GMFFBoss in response to a
GMFFInitialize
RunParm.
printTypesettingDefinitions
- prints data from Metamath $t Comments
for which there are GMFFExportParms
with matching
typesetDefs
(we don't load data from the $t's unless
it is needed.)GMFFException
- if an error occurredpublic void accumInputGMFFExportParms(GMFFExportParms inputGMFFExportParms)
Also invokes forceReinitialization()
which sets
gmffInitialized = false
to force re-initialization of GMFF the
next time a service request is made.
This function is called by GMFFBoss
in response to a
GMFFExportParms
RunParm.
inputGMFFExportParms
- data from GMFFExportParms RunParm.public void accumInputGMFFUserTextEscapesList(GMFFUserTextEscapes inputGMFFUserTextEscapes)
Also invokes forceReinitialization()
which sets
gmffInitialized = false
to force re-initialization of GMFF the
next time a service request is made.
This function is called by GMFFBoss
in response to a
GMFFUserTextEscapes
RunParm.
inputGMFFUserTextEscapes
- data from GMFFUserTextEscapes RunParm.public void cacheTypesettingCommentForGMFF(java.lang.String comment)
Also invokes forceReinitialization()
which sets
gmffInitialized = false
to force re-initialization of GMFF the
next time a service request is made.
This function is called by LogicalSystem
during processing of a
LoadFile
RunParm.
comment
- String Metamath $t Comment statement as stored in
SrcStmt
(the "$(" and "$)" delimiters are removed at
this pointand the first token is "$t").public void setInputGMFFUserExportChoice(GMFFUserExportChoice choice)
GMFFUserExportChoice
from one RunParm
for later validation and use.
Also invokes forceReinitialization()
which sets
gmffInitialized = false
to force re-initialization of GMFF the
next time a service request is made.
This function is called by GMFFBoss
in response to a
GMFFUserExportChoice
RunParm.
choice
- from GMFFUserExportChoice RunParm.public void setSymTbl(java.util.Map<java.lang.String,Sym> symTbl)
symTbl
for use in generating GMFF exports.
This function is called by the LogicalSystem
constructor -- which
itself is excuted during processing of the first LoadFile
RunParm. symTbl
is itself constructed during construction of
LogicalSystem
so this function is necessary even though
GMFFManager
is passed as an argument to the LogicalSystem
constructor (a somewhat circular arrangement.)
symTbl
is needed because an error message is generated when a
symbol to be typeset is not found in the Metamath $t definitions, but
only if the symbol string is really a valid symbol (and is not a
WorkVar
.) (GMFF not not require that Proof Worksheets be valid,
just that the Proof Worksheet format is loosely followed.)
symTbl
- The Symbol Table Map from LogicalSystem
public java.util.Map<java.lang.String,Sym> getSymTbl()
symTbl
for use in generating GMFF exports.symTbl
from LogicalSystem
public Messages getMessages()
messages
object.public boolean isGMFFInitialized()
gmffInitialized
boolean variable.public void forceReinitialization()
gmffInitialized
to false
.public void exportFromFolder(java.lang.String inputDirectory, java.lang.String theoremLabelOrAsterisk, java.lang.String inputFileType, java.lang.String maxNumberToExport, java.lang.String appendFileNameIn) throws GMFFException
This function implements the GMFFExportFromFolder
RunParm
command.
The sort sequence used to select and output Proof Worksheets is File Name minus File Type.
Refer to mmj2\doc\gmffdoc\C:\mmj2jar\GMFFDoc\GMFFRunParms.txt for more
info about the parameters on the GMFFExportFromFolder
RunParm.
inputDirectory
- The Directory to export Proof Worksheets fromtheoremLabelOrAsterisk
- Either a theorem label or "*". If theorem
label input then that is used as the starting point, otherwise
processing begins at the first file in the directory.inputFileType
- File Type to select, including the "." (e.g. ".mmp")maxNumberToExport
- Limits the number of exports processed. Must be
greater than zero and less then 2 billionish...appendFileNameIn
- Specifies an append-mode file name to which all
of the exported proofs will be written -- within the folder
specified for each Export Type on the GMFFExportParms RunParm;
overrides the normal name assigned to an export file.GMFFException
- if errors encountered.public void exportTheorem(java.lang.String theoremLabelOrAsterisk, java.lang.String maxNumberToExport, java.lang.String appendFileNameIn, ProofAsst proofAsst) throws GMFFException
LogicalSystem
.
This function implements the GMFFExportTheorem
RunParm command.
The sort sequence used to select and output thereoms is MObj.seq
-- that is, order of appearance in the LogicalSystem
.
Refer to mmj2\doc\gmffdoc\C:\mmj2jar\GMFFDoc\GMFFRunParms.txt for more
info about the parameters on the GMFFExportThereom
RunParm.
theoremLabelOrAsterisk
- Either a theorem label or "*". If theorem
label input then that is used as the starting point, otherwise
processing begins at the first file in the directory.maxNumberToExport
- Limits the number of exports processed. Must be
greater than zero and less then 2 billionish...appendFileNameIn
- Specifies an append-mode file name to which all
of the exported proofs will be written -- within the folder
specified for each Export Type on the GMFFExportParms RunParm;
overrides the normal name assigned to an export file.proofAsst
- The ProofAsst
object, used to format Proof
Worksheets from Metamath (RPN) proofs.GMFFException
- is errors encountered.public void gmffExportOneTheorem(Theorem theorem, java.lang.String appendFileName, ProofAsst proofAsst) throws GMFFException
Theorem
from the LogicalSystem
. loaded
This function is called by other functions in GMFFManager
but it
would be perfectly valid to call it externally.
This function calls ProofAsst.exportOneTheorem
which creates a
Proof Worksheet from a Metamath (RPN) proof. If the theorem's proof is
incomplete or invalid, or if it contains no assertions, an error message
results (and if input argument theorem
is null an
IllegalArgumentException
will result ;-)
theorem
- Theorem
to be exported.appendFileName
- Specifies an append-mode file name to which
exported proof will be written -- within the folder specified
for each Export Type on the GMFFExportParms RunParm; overrides
the normal name assigned to an export file.proofAsst
- The ProofAsst
object, used to format Proof
Worksheets from Metamath (RPN) proofs.GMFFException
- is errors encountered.public void gmffExportOneTheorem(java.lang.String theoremLabel, java.lang.String appendFileName, ProofAsst proofAsst) throws GMFFException
Theorem
from the LogicalSystem
. loaded
This function is called by other functions in GMFFManager
but it
would be perfectly valid to call it externally.
This function calls ProofAsst.exportOneTheorem
which creates a
Proof Worksheet from a Metamath (RPN) proof. If the theorem's proof is
incomplete or invalid, or if it contains no assertions, an error message
results -- and if input argument theoremLabel
is null or invalid
an exception is thrown...
theoremLabel
- label of Theorem
to be exported.appendFileName
- Specifies an append-mode file name to which
exported proof will be written -- within the folder specified
for each Export Type on the GMFFExportParms RunParm; overrides
the normal name assigned to an export file.proofAsst
- The ProofAsst
object, used to format Proof
Worksheets from Metamath (RPN) proofs.GMFFException
- is errors encountered.public java.util.List<GMFFException> exportProofWorksheet(java.lang.String proofText, java.lang.String appendFileName) throws GMFFException
This function is called by ProofAsst
and by various functions in
GMFFManager
.
The following functions are performed:
ProofWorksheetCache
object
ProofWorksheetCache
and accumulating confirmation messages from
them in return.
proofText
- String containing text in the format of an mmj2 Proof
Worksheet.appendFileName
- name of a file to which export data should be
appended (in the proper directory for the Export Type), or
null
if GMFF is supposed to generate the name.GMFFException
- if error found.public void parseMetamathTypesetComment(java.lang.String typesetDefKeyword, java.lang.String myDirectory, java.lang.String myMetamathTypesetCommentFileName, boolean runParmPrintOption) throws GMFFException
This function is primarily used for testing. It parses a file containing a single Metamath comment statement -- of the $t variety. Because it is intended for standalone use in testing, it does not require GMFF initialization prior to use, and it does not check for or trigger GMFF initialization.
The code is quick and dirty because it is just used for testing. Efficiency not an issue.
typesetDefKeyword
- The Metamath $t keyword to select for parsing
(e.g. "htmldef")myDirectory
- The directory containing the Metamath .mm file to
parse.myMetamathTypesetCommentFileName
- File Name in myDirectory to
parse.runParmPrintOption
- if true prints the input, including the
directory, file name, typesetDefKeyword and the entire
Metamath file.GMFFException
- if errors found.public void generateInitializationAuditReport()
public void generateTypesettingDefinitionsReport()