public class TMFFBoss extends Boss
TMFF is a sub-system used primarily in Proof Assistant but also in Dump, and wherever formulas are formatted. Therefore, it is not invoked directly by RunParms, but by services which use its services.
A reference to TMFFPreferences is stored *inside* TMFFPreferences, primarily for convenience in passing parameters to its main customer :) However, TMFFPreferences can live outside of TMFFPreferences and this code needs to maintain situational awareness of the state of the system. Specifically, TMFF relies upon .mm statements being parsed before TMFF formatting. Also, in the future it may be that an enhancement to TMFF which uses TMFFScheme assignents at the level of individual Syntax Axioms will be added. This would quite possibly involve storing information about the TMFFSchemes in an array -- one element for each TMFFFormat -- inside mmj.lang.Axiom so that TMFF can directly access the correct TMFFMethod without doing a lookup. In that event the loading and parsing of a new .mm file would be of critical interest as it would require re-application of updates to the Syntax mmj.lang.Axiom objects. (Programmatically this could be handled by the GrammarBoss notifying the TMFFBoss -- who would do nothing if TMFFPreferences is not already in existence, but if it is, then it would re-apply any syntax axiom-related updates.)
Other notes:
batchFramework, runParm
Constructor and Description |
---|
TMFFBoss(BatchFramework batchFramework)
Constructor with BatchFramework for access to environment.
|
Modifier and Type | Method and Description |
---|---|
protected TMFFPreferences |
buildTMFFPreferences()
Construct TMFFPreferences object from scratch.
|
protected void |
checkTMFFCanBeRunNow()
Check that TMFF can be run now.
|
protected void |
editTMFFDefineFormat()
TMFFDefineFormat RunParm validation and loading.
|
protected void |
editTMFFDefineScheme()
TMFFDefineScheme RunParm validation and loading.
|
protected void |
editTMFFUseFormat(Setting<java.lang.Integer> setting)
TMFFUseFormat RunParm validation and loading.
|
TMFFPreferences |
getTMFFPreferences()
Fetches a reference to the TMFFPreferences, first initializing it if
necessary.
|
accumException, addContext, buildBufferedFileReader, buildBufferedFileWriter, buildPrintWriter, doRunParmCommand, error, error, error, get, getBoolean, getBoolean, getColor, getEnum, getExistingFile, getExistingFile, getExistingFolder, getExistingFolder, getFileCharset, getFileName, getFileNameSuffix, getFileUsage, getInt, getNonBlank, getNonnegInt, getOnOff, getPosInt, getPrintableNoBlanksString, getPrintWriter, getSelectorCount, getSelectorTheorem, getStmt, getTheorem, getYesNo, opt, parseInt, putCommand, putCommand, require
public TMFFBoss(BatchFramework batchFramework)
batchFramework
- for access to environment.protected void editTMFFDefineScheme()
protected void editTMFFDefineFormat()
protected void editTMFFUseFormat(Setting<java.lang.Integer> setting)
setting
- The setting to adjustpublic TMFFPreferences getTMFFPreferences()
protected TMFFPreferences buildTMFFPreferences()
protected void checkTMFFCanBeRunNow()
In fact, if the grammar is not pre-initialized when the instruction pointer reaches this code, a Exception is thrown. The rationale is that ProofAsstBoss will check grammar initialization before invoking this anyway, and we'll just make the user fix the problem for other invocations before doing anything else. This will save having to check if 'tmffPreferences == null' everywhere else. Ugly, but...