public class ProofAsstBoss extends Boss
batchFramework, runParm
Constructor and Description |
---|
ProofAsstBoss(BatchFramework batchFramework)
Constructor with BatchFramework for access to environment.
|
Modifier and Type | Method and Description |
---|---|
void |
doPreprocessRequestBatchTest()
Exercises the PreprocessRequest code.
|
void |
doProofAsstAutocompleteEnabled()
If this option is set then the proof assistant will support autocomplete
derivation steps
|
void |
doProofAsstBatchTest()
Reads and unifies theorem proofs in test mode.
|
void |
doProofAsstDeriveAutocomplete()
If this option is set then the proof assistant will support autocomplete
derivation steps
|
void |
doProofAsstExportToFile()
Exports currently loaded theorem proofs to an export file.
|
void |
doProofAsstTheoremSearchOptimization()
Perform the optimizations for theorem search during "parallel"
unification
|
void |
doProofAsstUseAutotransformations()
Perform the initialization of auto-transformation component.
|
void |
doRunProofAsstGUI()
Executes the RunProofAsstGUI command, prints any messages, etc.
|
void |
doSetMMDefinitionsCheck()
Deprecated.
Use
MacroManager.runMacro(ExecutionMode, String[])
with macro definitionCheck . |
void |
doStepSelectorBatchTest()
Exercises the StepSelectorSearch code.
|
protected void |
editProofAsstAssrtListFreespace()
Validate ProofAsstAssrtListFreespace.
|
protected void |
editProofAsstAutoReformat()
Validate ProofAsstAutoReformat RunParm.
|
protected void |
editProofAsstBackgroundColorRGB()
Validate ProofAsstBackgroundColorRGB RunParm.
|
protected void |
editProofAsstDefaultFileNameSuffix()
Validate Proof Assistant Default File Name Suffix
|
protected void |
editProofAsstDjVarsSoftErrors()
edit ProofAsstDjVarsSoftErrors RunParm.
|
protected void |
editProofAsstErrorMessageColumns()
Validate ProofAsstErrorMessageColumns
|
protected void |
editProofAsstErrorMessageRows()
Validate ProofAsstErrorMessageRows
|
protected void |
editProofAsstExcludeDiscouraged()
Validate ProofAsstAutoReformat RunParm.
|
protected void |
editProofAsstFontBold()
Validate ProofAsstFontBold RunParm.
|
protected void |
editProofAsstFontFamily()
Validate ProofAsstFontFamily RunParm.
|
protected void |
editProofAsstFontSize()
Validate ProofAsstFontSize RunParm.
|
protected void |
editProofAsstForegroundColorRGB()
Validate ProofAsstForegroundColorRGB RunParm.
|
protected void |
editProofAsstFormulaLeftCol()
Validate ProofAsstFormulaLeftCol.
|
protected void |
editProofAsstFormulaRightCol()
Validate ProofAsstFormulaRightCol.
|
protected void |
editProofAsstHighlightingEnabled()
Validate ProofAsstHighlightingEnabled RunParm.
|
protected void |
editProofAsstHighlightingStyle()
Validate ProofAsstHighlightingEnabled RunParm.
|
protected void |
editProofAsstIncompleteStepCursor()
edit ProofAsstIncompleteStepCursor RunParm.
|
protected void |
editProofAsstLineSpacing()
Validate ProofAsstLineSpacing RunParm.
|
protected void |
editProofAsstLookAndFeel()
edit ProofAsstLookAndFeel RunParm.
|
protected void |
editProofAsstMaximized()
Validate ProofAsstMaximized RunParm.
|
protected void |
editProofAsstOutputCursorInstrumentation()
Validate ProofAsstOutputCursorInstrumentation RunParm.
|
protected void |
editProofAsstProofFolder()
Validate Proof Assistant Proof Folder Runparm.
|
protected void |
editProofAsstProofFormat()
edit ProofAsstProofFormat RunParm.
|
protected void |
editProofAsstRPNProofLeftCol()
Validate ProofAsstRPNProofLeftCol.
|
protected void |
editProofAsstRPNProofRightCol()
Validate ProofAsstRPNProofRightCol.
|
protected void |
editProofAsstStartupProofWorksheet()
Validate Proof Assistant Startup Proof Worksheet Runparm.
|
protected void |
editProofAsstTextAtTop()
Validate ProofAsstTextAtTop RunParm.
|
protected void |
editProofAsstTextColumns()
Validate ProofAsstTextColumns
|
protected void |
editProofAsstTextRows()
Validate ProofAsstTextRows
|
protected void |
editProofAsstUndoRedoEnabled()
Validate ProofAsstUndoRedoEnabled RunParm.
|
protected void |
editProofAsstUnifySearchExclude()
Validate ProofAsstUnifySearchExclude
|
protected void |
editRecheckProofAsstUsingProofVerifier()
Validate RecheckProofAsstUsingProofVerifier
|
protected void |
editStepSelectorDialogPaneHeight()
Validate StepSelectorDialogPaneHeight.
|
protected void |
editStepSelectorDialogPaneWidth()
Validate StepSelectorDialogPaneWidth.
|
protected void |
editStepSelectorMaxResults()
Validate StepSelectorMaxResults
|
protected void |
editStepSelectorShowSubstitutions()
Validate StepSelectorShowSubstitutions
|
protected boolean |
getAsciiRetest(int valueFieldNbr)
Validate Proof Assistant AsciiRetest Parm.
|
protected boolean |
getCompareDJs(int valueFieldNbr)
Validate Proof Assistant Import CompareDJs Parm ("CompareDJs" or
"NoCompareDJs" or "").
|
protected boolean |
getDeriveFormulas(int valueFieldNbr)
Validate Proof Assistant Export DeriveFormulas Parm ("DeriveFormulas" or
"NoDeriveFormulas" or "").
|
protected java.io.BufferedWriter |
getExportFile()
Validate output ProofAsst Export File RunParm options and returns
FileWriter object
|
protected boolean |
getExportFormatUnified(int valueFieldNbr)
Validate Proof Assistant Export Format Parm ("unified" or "un-unified").
|
protected HypsOrder |
getHypsOrder(int valueFieldNbr)
Validate Proof Assistant Export Hyps Order Parm ("Correct", "Randomized",
"Reverse" ,and others (see
HypsOrder ). |
java.io.Reader |
getImportFile(int valueFieldNbr)
Validate input ProofAsst Import File RunParm option and returns Buffered
File Reader object.
|
protected boolean |
getPrintParm(int valueFieldNbr)
Validate Proof Assistant Export Print Parm ("Print" or "NoPrint").
|
ProofAsst |
getProofAsst()
Fetch a ProofAsst object.
|
ProofAsstPreferences |
getProofAsstPreferences()
Fetches a reference to the ProofAsstPreferences, first initializing it if
necessary.
|
protected boolean |
getUpdateDJs(int valueFieldNbr)
Validate Proof Assistant Import UpdateDJs Parm ("UpdateDJs" or
"NoUpdateDJs" or "").
|
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 ProofAsstBoss(BatchFramework batchFramework)
batchFramework
- for access to environment.public ProofAsst getProofAsst()
protected void editProofAsstLookAndFeel()
protected void editProofAsstDjVarsSoftErrors()
protected void editProofAsstProofFormat()
protected void editProofAsstIncompleteStepCursor()
protected void editProofAsstHighlightingEnabled()
protected void editProofAsstHighlightingStyle()
protected void editProofAsstForegroundColorRGB()
protected void editProofAsstBackgroundColorRGB()
protected void editProofAsstFontSize()
protected void editProofAsstFontFamily()
protected void editProofAsstFontBold()
protected void editProofAsstLineSpacing()
protected void editProofAsstTextColumns()
protected void editProofAsstTextRows()
protected void editProofAsstErrorMessageRows()
protected void editProofAsstErrorMessageColumns()
protected void editProofAsstMaximized()
protected void editProofAsstTextAtTop()
protected void editProofAsstFormulaLeftCol()
protected void editProofAsstFormulaRightCol()
protected void editProofAsstRPNProofLeftCol()
protected void editProofAsstRPNProofRightCol()
protected void editStepSelectorMaxResults()
Must be positive integer.
protected void editStepSelectorShowSubstitutions()
Must be yes, no, on, off, true, false.
protected void editStepSelectorDialogPaneWidth()
protected void editStepSelectorDialogPaneHeight()
protected void editProofAsstAssrtListFreespace()
protected void editProofAsstDefaultFileNameSuffix()
protected void editProofAsstProofFolder()
protected void editProofAsstStartupProofWorksheet()
protected void editProofAsstOutputCursorInstrumentation()
protected void editProofAsstAutoReformat()
protected void editProofAsstUndoRedoEnabled()
protected void editRecheckProofAsstUsingProofVerifier()
protected void editProofAsstUnifySearchExclude()
protected void editProofAsstExcludeDiscouraged()
public void doProofAsstExportToFile()
public void doProofAsstBatchTest()
public void doProofAsstTheoremSearchOptimization()
public void doProofAsstUseAutotransformations()
public void doProofAsstAutocompleteEnabled()
public void doProofAsstDeriveAutocomplete()
public void doStepSelectorBatchTest()
public void doPreprocessRequestBatchTest()
@Deprecated public void doSetMMDefinitionsCheck()
MacroManager.runMacro(ExecutionMode, String[])
with macro definitionCheck
.public java.io.Reader getImportFile(int valueFieldNbr)
valueFieldNbr
- option number of file namejava.lang.IllegalArgumentException
- if an error occurredprotected java.io.BufferedWriter getExportFile()
java.lang.IllegalArgumentException
- if an error occurredprotected boolean getExportFormatUnified(int valueFieldNbr)
valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredprotected HypsOrder getHypsOrder(int valueFieldNbr)
HypsOrder
).valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredprotected boolean getDeriveFormulas(int valueFieldNbr)
valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredprotected boolean getCompareDJs(int valueFieldNbr)
valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredprotected boolean getUpdateDJs(int valueFieldNbr)
valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredprotected boolean getAsciiRetest(int valueFieldNbr)
valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredprotected boolean getPrintParm(int valueFieldNbr)
valueFieldNbr
- number of field in RunParm line.java.lang.IllegalArgumentException
- if an error occurredpublic void doRunProofAsstGUI()
java.lang.IllegalArgumentException
- if an error occurredpublic ProofAsstPreferences getProofAsstPreferences()
Note: must re-initialize the TMFFPreferences reference in ProofAsstPreferences because TMFFBoss controls which instance of TMFFPreferences is active!!!