public class TMFFPreferences
extends java.lang.Object
NOTE: this holds a couple of elements that were originally part of Proof Assistant's preferences, but now an instance of TMFFPreferences is stored inside of ProofAsstPreferences.
Modifier and Type | Field and Description |
---|---|
Setting<java.lang.Integer> |
altFormatNbr |
Setting<java.lang.Integer> |
altIndent |
Setting<java.lang.Integer> |
currFormatNbr |
Setting<java.lang.Integer> |
formulaLeftCol
Formula left column used in formatting proof text areas.
|
Setting<java.lang.Integer> |
formulaRightCol
Formula right column used in formatting proof text areas.
|
Setting<java.lang.Boolean> |
inAltFormatNow |
Setting<java.lang.Boolean> |
lineWrap
Line wrap on or off.
|
Setting<java.lang.Integer> |
prevFormatNbr |
Setting<java.lang.Integer> |
prevIndent |
Setting<java.lang.Integer> |
textColumns
Number of text columns used to display formulas.
|
Setting<java.lang.Integer> |
textRows
Number of text rows used to display formulas.
|
Setting<java.lang.Integer> |
useIndent |
Constructor and Description |
---|
TMFFPreferences(SessionStore store)
Default constructor for TMFFPreferences.
|
Modifier and Type | Method and Description |
---|---|
boolean |
addDefinedScheme(TMFFScheme s)
Add newly defined Scheme to Preferences data.
|
TMFFFormat |
getCurrFormat()
Returns the TMFFFormat presently in use.
|
TMFFScheme |
getDefinedScheme(java.lang.String definedSchemeName)
Get already defined Scheme from Preferences data.
|
java.lang.String |
getFormatListString()
A simple routine to build a list of all defined Formats.
|
TMFFFormat |
getTMFFUnformattedFormat()
Returns the default Format.
|
TMFFScheme |
getTMFFUnformattedScheme()
Returns the default Scheme
|
boolean |
isTMFFEnabled()
Informs the caller whether or not TMFF is enabled.
|
int |
renderFormula(TMFFStateParams tmffSP,
ParseTree parseTree,
Formula formula)
Formats a formula and outputs it to a StringBuilder using the given
ParseTree, Formula and TMFFStateParams instance.
|
int |
renderFormula(TMFFStateParams tmffSP,
ParseTree parseTree,
Formula formula,
int proofLevel)
Formats a formula and outputs it to a StringBuilder using the given
ParseTree, Formula and TMFFStateParams instance.
|
void |
toggleAltFormatAndIndentParms()
Toggles the alternate and current format and indent parameters when the
ProofAsstGUI Reformat Proof Swap Alt menu item is selected.
|
void |
updateDefinedFormat(TMFFFormat newFormat)
Update existing Format definition.
|
void |
updateDefinedScheme(TMFFScheme newScheme)
Update existing Scheme definition.
|
boolean |
updateMaxDepthAcrossMethods(int maxDepth)
Updates maxDepth for all TMFFMethods that allow updates.
|
int |
validateIndentString(java.lang.String s)
A slightly redundant routine to validate an input indent amount.
|
public Setting<java.lang.Integer> formulaLeftCol
public Setting<java.lang.Integer> formulaRightCol
public Setting<java.lang.Integer> textColumns
This number is used to line wrapping and basically corresponds to the window used to display formulas.
A formula can be longer than this number, and the Frame should scroll -- assuming that lineWrap is off and there are no NewLines.
public Setting<java.lang.Integer> textRows
public Setting<java.lang.Boolean> lineWrap
If line wrap is on then Newlines (carriage returns) will not be used to split formulas. Instead, space characters will be written to fill out the remaining text columns on the line.
public Setting<java.lang.Integer> currFormatNbr
public Setting<java.lang.Integer> altFormatNbr
public Setting<java.lang.Integer> useIndent
public Setting<java.lang.Integer> altIndent
public Setting<java.lang.Boolean> inAltFormatNow
public Setting<java.lang.Integer> prevFormatNbr
public Setting<java.lang.Integer> prevIndent
public TMFFPreferences(SessionStore store)
store
- The session storepublic boolean isTMFFEnabled()
In practice "enabled" means using Format 1, 2 or 3 -- and "disabled" means using Format 0.
Although TMFF's renderFormula can be invoked even if TMFF is disabled, in ProofWorksheet considerable work is needed to parse formulas from Derivation Proof Steps for exported proofs. Therefore, if TMFF is disabled the grammatical parsing process can be skipped.
public int renderFormula(TMFFStateParams tmffSP, ParseTree parseTree, Formula formula, int proofLevel)
This is intended to be the main way of invoking TMFF formatting.
tmffSP
- TMFFStateParams initialized, ready for use.parseTree
- of the Formula to be rendered. If left null, the formula
will be output in unformatted mode.formula
- to be formatted and output to sb.proofLevel
- level number of formula in proof.public int renderFormula(TMFFStateParams tmffSP, ParseTree parseTree, Formula formula)
This is the *old* method for which proof level is not used. It is used when the caller wishes to set Formula Left Column independently in tmffSP.
tmffSP
- TMFFStateParams initialized, ready for use.parseTree
- of the Formula to be rendered. If left null, the formula
will be output in unformatted mode.formula
- to be formatted and output to sb.public TMFFFormat getCurrFormat()
public TMFFFormat getTMFFUnformattedFormat()
public TMFFScheme getTMFFUnformattedScheme()
public int validateIndentString(java.lang.String s) throws TMFFException
This routine is used by ProofAsstGUI.
s
- Indent amountString.TMFFException
- if input is invalid.public java.lang.String getFormatListString()
The display is returned as a String consisting of lines terminated with newline characters, where each line consists of Format Number + " - " + Scheme Name.
This routine is used by ProofAsstGUI.
public void toggleAltFormatAndIndentParms()
What that will accomplish is that the "prev" items are set only when you go *int* alt mode and are restored when you come out of alt mode. So if the user is in alt mode and then changes the format nbr or indent amount -- reformatting -- and then selects "...Swap Alt", the original format nbr and indent amount *before* going into alt mode are restored...which is a good thing since it lets the user play around and then return to a good setting, while leaving the alt format and indent settings unchanged (they are only changed by RunParm.)
public boolean addDefinedScheme(TMFFScheme s)
s
- TMFFScheme to be added to the TMFFPreferences data.public void updateDefinedFormat(TMFFFormat newFormat)
newFormat
- to store into the Preferences data.public void updateDefinedScheme(TMFFScheme newScheme)
Updates each Format that uses the existing Scheme Name to point to the new object. (It has to do a replace because the object type could theoretically be different -- for example, "TMFFFlat" instead of "TMFFAlignColumn".)
newScheme
- to update into the Preferences data.public TMFFScheme getDefinedScheme(java.lang.String definedSchemeName)
definedSchemeName
- to be looked up.public boolean updateMaxDepthAcrossMethods(int maxDepth)
As of the initial release, only TMFFAlignColumn uses maxDepth. The methods TMFFFlat and TMFFUnformatted have maxDepth = Integer.MAX_VALUE which results in no maxDepth line breaks from happening -- therefore, they do not allow updates after initial construction of the method.
maxDepth
- parameter.