public class ProofAsstPreferences
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
Setting<java.lang.Integer> |
assrtListFreespace |
Setting<java.lang.Boolean> |
autocomplete |
Setting<java.lang.Boolean> |
autoReformat
Boolean value enabling or disabling AutoReformat of proof step formulas
after Work Variables are resolved.
|
Setting<java.awt.Color> |
backgroundColor
Background color for Proof Asst GUI.
|
Setting<java.awt.Rectangle> |
bounds
Proof GUI on-screen location.
|
Setting<java.lang.String> |
defaultFileNameSuffix
Default file name suffix, such as ".txt" or ".mmp".
|
Setting<java.lang.Boolean> |
deriveAutocomplete |
Setting<PaConstants.DjVarsSoftErrors> |
djVarsSoftErrors |
Setting<java.lang.Integer> |
errorMessageColumns
Number of error message columns on the ProofAsstGUI.
|
Setting<java.lang.Integer> |
errorMessageRows
Number of error message rows on the ProofAsstGUI.
|
Setting<java.lang.Boolean> |
excludeDiscouraged
True if discouraged theorems are being excluded from unification search
|
Setting<java.lang.Boolean> |
exportDeriveFormulas
On/off indicator instructing the Proof Assistant Export to output blank
formulas -- or not -- for non-qed derivation steps (not logical hyps).
|
Setting<java.lang.Boolean> |
exportFormatUnified
On/off indicator instructing the Proof Assistant Export to use unified or
"un-unified" format for exported proofs.
|
Setting<HypsOrder> |
exportHypsOrder
Set the order in which the Proof Assistant Export should output proof
step logical hypotheses (a testing feature for Proof Assistant.)
|
Setting<java.lang.Boolean> |
fontBold
Font Bold style parameter used in ProofAsstGUI.
|
Setting<java.lang.String> |
fontFamily
Font Family Name used in ProofAsstGUI.
|
Setting<java.lang.Integer> |
fontSize
Font size used in ProofAsstGUI.
|
Setting<java.awt.Color> |
foregroundColor
Foreground color for Proof Asst GUI.
|
java.util.Map<java.lang.String,javax.swing.text.SimpleAttributeSet> |
highlighting |
Setting<java.lang.Boolean> |
highlightingEnabled
Syntax highlighting for Proof Asst GUI.
|
Setting<java.lang.Boolean> |
importCompareDJs
On/off indicator instructing the Proof Assistant Batch Test Import to
compare generated Dj Vars with the originals.
|
Setting<java.lang.Boolean> |
importUpdateDJs
On/off indicator instructing the Proof Assistant Batch Test Import to
update the originals that are stored in memory (does not update the .mm
file though.)
|
Setting<PaConstants.IncompleteStepCursor> |
incompleteStepCursor |
Setting<java.lang.Float> |
lineSpacing
Line spacing used in ProofAsstGUI.
|
Setting<java.lang.Boolean> |
maximized
Proof Maximized option for ProofAsstGUI.
|
Setting<java.lang.Boolean> |
outputCursorInstrumentation
Boolean value enabling or disabling "instrumentation" of the OutputCursor
for regression testing.
|
Setting<java.io.File> |
proofFolder
Proof folder used for storing proof text areas in ProofAsstGUI.
|
Setting<PaConstants.ProofFormat> |
proofFormat |
Setting<java.lang.String> |
proofTheoremLabel |
Setting<java.lang.Boolean> |
recheckProofAsstUsingProofVerifier
On/off indicator instructing Proof Assistant to double-check every proof
steps generated proof tree using the Proof Engine (
VerifyProofs ). |
Setting<java.lang.Integer> |
rpnProofLeftCol
Get left column number for RPN statement labels when creating
ProofAsstWorksheet.GeneratedProofStmt
|
Setting<java.lang.Integer> |
rpnProofRightCol
Set right column number for RPN statement labels when creating
ProofAsstWorksheet.GeneratedProofStmt
|
Setting<java.io.File> |
startupProofWorksheetFile
Startup Proof Worksheet File to be displayed when the ProofAsstGUI is
first displayed.
|
Setting<java.lang.Integer> |
stepSelectorDialogPaneHeight |
Setting<java.lang.Integer> |
stepSelectorDialogPaneWidth |
Setting<java.lang.Integer> |
stepSelectorMaxResults |
Setting<java.lang.Boolean> |
stepSelectorShowSubstitutions |
Setting<java.lang.Boolean> |
textAtTop
Proof Text At Top option for ProofAsstGUI.
|
TMFFPreferences |
tmffPreferences |
Setting<java.lang.Boolean> |
undoRedoEnabled
Boolean value enabling or disabling use of Undo/Redo Menu Items on the
Proof Assistant GUI.
|
Setting<java.util.Set<java.lang.String>> |
unifySearchExclude
Array of assertions that will be excluded from the proof unification
search process.
|
Constructor and Description |
---|
ProofAsstPreferences()
Default constructor.
|
ProofAsstPreferences(SessionStore store)
Constructor with pre-constructed storage manager.
|
Modifier and Type | Method and Description |
---|---|
java.lang.String |
getFontListString()
A simple routine to build a list of all defined Fonts Families.
|
javax.swing.text.AttributeSet |
getHighlightingStyle(java.lang.String key)
Gets syntax highlighting for Proof Asst GUI.
|
SearchMgr |
getSearchMgr() |
StepUnifier |
getStepUnifier()
Get StepUnifier.
|
StepUnifier |
getStepUnifierInstance()
Get StepUnifier Instance.
|
SessionStore |
getStore() |
WorkVarManager |
getWorkVarManager()
Get WorkVarManager.
|
static boolean |
parseBoolean(java.lang.String s)
A stupid routine to validate StepSelectorShowSubstitutions.
|
void |
setHighlightingStyle(java.lang.String key,
java.awt.Color color,
java.lang.Boolean bold,
java.lang.Boolean italic)
Sets syntax highlighting for Proof Asst GUI.
|
void |
setSearchMgr(SearchMgr searchmgr) |
void |
setStepUnifier(StepUnifier stepUnifier)
Set StepUnifier
|
void |
setWorkVarManager(WorkVarManager workVarManager)
Set WorkVarManager
|
java.lang.String |
validateFontFamily(java.lang.String familyName)
A stupid routine to validate a Font Family Name.
|
public TMFFPreferences tmffPreferences
public Setting<java.io.File> proofFolder
public Setting<java.io.File> startupProofWorksheetFile
public Setting<java.lang.String> defaultFileNameSuffix
public Setting<java.lang.Integer> fontSize
NOTE: presently, font size is set in ProofAsstBoss as part of the start-up of ProofAsstGUI, based on a RunParm. Then during operation of ProofAsstGUI the user can increase or decrease the font size used, and those settings propagate to these ProofAsstPreferences (but are not stored externally for use in the next session -- permanent setting should be made in the RunParm file.)
public Setting<java.lang.String> fontFamily
Note: Proof Assistant formatting of formulas (via TMFF) REQUIRES a fixed-width font for symbol alignment! A proportional or variable-width font can be used but symbol alignments may be off.
Note: The default is "Monospaced", which works just fine...
public Setting<java.lang.Boolean> fontBold
public Setting<java.lang.Float> lineSpacing
public Setting<java.lang.Integer> errorMessageRows
public Setting<java.lang.Integer> errorMessageColumns
public Setting<java.lang.Boolean> maximized
public Setting<java.lang.Boolean> textAtTop
public Setting<java.awt.Rectangle> bounds
public Setting<java.lang.Integer> rpnProofLeftCol
public Setting<java.lang.Integer> rpnProofRightCol
public Setting<java.lang.Boolean> recheckProofAsstUsingProofVerifier
VerifyProofs
).public Setting<java.lang.Boolean> exportFormatUnified
Note: this applies to exported proofs written via ProofAsst.exportToFile, which is triggered via BatchMMJ2 "RunParm ProofAsstExportToFile" as well as the "ProofAsstBatchTest" (the latter when no input file is specified and an "export to memory" is implicitly requested.)
public Setting<HypsOrder> exportHypsOrder
Note: this applies to exported proofs written via ProofAsst.exportToFile, which is triggered via BatchMMJ2 "RunParm ProofAsstExportToFile" as well as the "ProofAsstBatchTest" (the latter when no input file is specified and an "export to memory" is implicitly requested.)
public Setting<java.lang.Boolean> exportDeriveFormulas
Note: this applies to exported proofs written via ProofAsst.exportToFile, which is triggered via BatchMMJ2 "RunParm ProofAsstExportToFile" as well as the "ProofAsstBatchTest" (the latter when no input file is specified and an "export to memory" is implicitly requested.)
public Setting<java.lang.Boolean> importCompareDJs
public Setting<java.lang.Boolean> importUpdateDJs
public Setting<java.util.Set<java.lang.String>> unifySearchExclude
This feature is primarily needed for redundant theorems that are carried in a Metamath database because they have a different proof (other possibilities exist.)
public Setting<java.lang.Boolean> excludeDiscouraged
public Setting<java.lang.Integer> stepSelectorMaxResults
public Setting<java.lang.Boolean> stepSelectorShowSubstitutions
public Setting<java.lang.Integer> stepSelectorDialogPaneWidth
public Setting<java.lang.Integer> stepSelectorDialogPaneHeight
public Setting<java.lang.Integer> assrtListFreespace
public Setting<java.lang.Boolean> outputCursorInstrumentation
public Setting<java.lang.Boolean> autoReformat
public Setting<java.lang.Boolean> undoRedoEnabled
public Setting<java.lang.Boolean> highlightingEnabled
public java.util.Map<java.lang.String,javax.swing.text.SimpleAttributeSet> highlighting
public Setting<java.awt.Color> foregroundColor
public Setting<java.awt.Color> backgroundColor
public Setting<PaConstants.DjVarsSoftErrors> djVarsSoftErrors
public Setting<PaConstants.ProofFormat> proofFormat
public Setting<PaConstants.IncompleteStepCursor> incompleteStepCursor
public Setting<java.lang.Boolean> autocomplete
public Setting<java.lang.Boolean> deriveAutocomplete
public Setting<java.lang.String> proofTheoremLabel
public ProofAsstPreferences()
public ProofAsstPreferences(SessionStore store)
store
- The storage managerpublic SessionStore getStore()
public void setHighlightingStyle(java.lang.String key, java.awt.Color color, java.lang.Boolean bold, java.lang.Boolean italic) throws java.lang.IllegalArgumentException
key
- The name of one of the styles of the syntax highlightingcolor
- the foreground colorbold
- true for bold, false for plain, null for inherititalic
- true for italic, false for plain, null for inheritjava.lang.IllegalArgumentException
- if thepublic javax.swing.text.AttributeSet getHighlightingStyle(java.lang.String key)
key
- the token typepublic void setWorkVarManager(WorkVarManager workVarManager)
workVarManager
- instance of WorkVarManager.public WorkVarManager getWorkVarManager()
public void setStepUnifier(StepUnifier stepUnifier)
stepUnifier
- instance of StepUnifier or null.public StepUnifier getStepUnifier()
public StepUnifier getStepUnifierInstance()
public java.lang.String getFontListString()
This routine is used by ProofAsstPreferences.
public java.lang.String validateFontFamily(java.lang.String familyName)
This routine is used by ProofAsstPreferences.
familyName
- font family name, which must be available in
GraphicsEnvironment.getAllFonts().java.lang.IllegalArgumentException
- if input familyName not installed in the
system.public static boolean parseBoolean(java.lang.String s) throws java.lang.IllegalArgumentException
This routine is used by ProofAsstGUI.
s
- yes or no or true or false or on or off.java.lang.IllegalArgumentException
- if invalid value.public SearchMgr getSearchMgr()
public void setSearchMgr(SearchMgr searchmgr)