Persistent Storage Of GUI Preferences

This feature enables mmj2 to remember your preferences, the choices you made to alter the appearance or functionality of the GUI part of mmj2, namely the Proof Assistant and related windows.

NOTE: window positions and sizes will be preserved across mmj2 sessions, but not window visibility -- at mmj2 start-up only the Proof Assistant GUI window will be displayed, and the other windows will be displayed when requested.

Previously users were required to input RunParm file commands to permanently alter the default preferences.

To implement this new feature a new RunParm command, "GUIPreferencesFile" is used to turn on Persistent Storage of GUI Preferences and to specify the file to be used:

LoadFile,set.mm
VerifyProof,*
Parse,*
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs
TheoremLoaderMMTFolder,myproofs
* <--RunParm commands here and defaults are overridden by GUIPreferencesFile
GUIPreferencesFile,GUIPreferences.txt
* <--RunParm commands here are permanent (override)Preferences
RunProofAsstGUI

About the GUIPreferencesFile:

The GUIPreferences file is stored by default in the mmj2Path directory (see mmj2/doc/mmj2CommandLineArguments.html) but a path can be specified on the GUIPreferencesFile RunParm (e.g. in Windows: "GUIPreferencesFile,c:\mydata\myGUIPreferences.txt").
The GUIPreferencesFile is formatted as a comma-delimited text file, like the RunParms.txt file, but with a necessary modification: by definition the last field of each line is delimited only by the end-of-line characters. This invention is necessary because the Search Options window fields may contain any valid ASCII character and this approach is simpler than defining escape character sequences.
To restore all of the mmj2 preference settings to the default values, simply delete your GUIPreferences file entirely or just its contents; mmj2 will recreate the file automatically at the end of your next mmj2 Proof Assistant session -- minus your old preferences.
The GUIPreferences file is updated by mmj2 upon exit from the mmj2 Proof Assistant -- except for unexpected program failures, which abruptly and abnormally terminate processing.
The GUIPreferences file is updated by mmj2 only with preferences that are different from the hardcoded mmj2 default settings, and only if changes were made during processing.
If mmj2 encounters an error in a GUIPreferences file command during startup, a pop-up error message is displayed, and then mmj2 restores the preference setting to the default value; upon exit the GUIPreferences file is "fixed" (i.e. you lose the saved preference...but don't worry, this should not happen unless you "text edit" your file and goof ...so make a backup if you're doing that...)
The contents of the GUIPreferences file are simply RunParm-style commands which override both the default preferences hardcoded into mmj2 and any RunParm.txt file commands previously processed.
New commands will be added to the system for the mmj2 Search Options preferences and history, but these may only be used inside the GUIPreferencesFile (because a different program processes them -- and because they are defined differently.)

NOTE TO READER: You can probably just quit reading now. The rest of the information is available if needed, and that will probably never happen...unless things go badly... :-)

EXISTING PROOF ASSISTANT GUI PREFERENCES

MENU OPTION / MECHANISM	RUNPARM / GUI PREFERENCES FILE COMMANDS W/DEFAULT
File/Save As	ProofAsstProofFolder,myproofs
Edit/Set Incomplete Step Cursor	ProofAsstIncompleteStepCursor,AsIs
Edit/Set Soft Dj Vars Error Handling	ProofAsstDjVarsSoftErrors,GenerateReplacements
Edit/Set Font Family	ProofAsstFontFamily,Monospaced
Edit/Font Style Plain/Bold	ProofAsstFontBold,yes
Edit/Set (Larger/Smaller) Font Size	ProofAsstFontSize,14
	`ProofAsstFormulaRightCol,79 ProofAsstTextColumns,80` (`ProofAsstFormulaRightCol` is being "deprecated" --> it will be accepted but the input value will be ignored. Instead the value will be computed as `ProofAsstTextColumns` minus 1.)
	`ProofAsstTextRows,25`
	`ProofAsstErrorMessageColumns,80` (This RunParm is being "deprecated" --> it will be accepted but the input value will be ignored. The number of error message columns on the screen will be the same as `ProofAsstTextColumns`.)
	`ProofAsstErrorMessageRows,4`
Edit/Set Foreground Color	ProofAsstForegroundColorRGB,0,0,0
Edit/Set Background Color	ProofAsstBackgroundColorRGB,255,255,255
Edit/Set Format Number	TMFFUseFormat,13
Edit/Set Indent Amount	TMFFUseIndent,0
Unify/Set Step Selector Max Results (This menu item will be removed from the Proof Assistant GUI window because it is available on the Search Options window).	StepSelectorMaxResults,50
Unify/Set Step Selector Show Substitutions (This menu item will be removed from the Proof Assistant GUI window because it is available on the Search Options window).	StepSelectorShowSubstitutions,true
TL/Set Theorem Loader MMT Folder	TheoremLoaderMMTFolder,myproofs
TL/Set Theorem Loader Dj Vars Option	TheoremLoaderDjVarsOption,NoUpdate
TL/Set Theorem Loader Audit Messages	TheoremLoaderAuditMessages,Yes
TL/Set Theorem Loader Store MM Indent Amount	TheoremLoaderStoreMMIndentAmt,2
TL/Set Theorem Loader Store MM Right Column	TheoremLoaderStoreMMRightCol,79
TL/Set Theorem Loader Store MM Formulas AsIs	TheoremLoaderStoreFormulasAsIs,Yes

(NEW) WINDOW SIZE/APPEARANCE PREFERENCES

MENU OPTION/MECHANISM	GUI PREFERENCES FILE COMMAND
Error Message Pane Window Control	`ErrorMessagePaneHeight,9999`
Proof Asst GUI Window Control, Location	`ProofAsstWindowLocationXY,9999,9999`
Proof Asst GUI Window Control, Width*	`ProofAsstFormulaRightCol,79 ProofAsstTextColumns,80`(`ProofAsstFormulaRightCol` is being "deprecated" --> it will be accepted but the input value will be ignored. Instead the value will be computed as `ProofAsstTextColumns` minus 1. )
Proof Asst GUI Window Control, Proof Pane Height*	`ProofAsstTextRows,25`
	`ProofAsstErrorMessageColumns,80` (This RunParm is being "deprecated" --> it will be accepted but the input value will be ignored. The number of error message columns on the screen will be the same as `ProofAsstTextColumns`.)
Proof Asst GUI Window Control, Error Message Pane Height*	`ProofAsstErrorMessageRows,4`
Search Options Window Control	`SearchOptionsWindowLocationXY,9999,9999`
Search Options Window Control	`SearchOptionsWindowWidth,9999`
Search Options Window Control	`SearchOptionsWindowHeight,9999`
Step Selector Dialog Window Control	`StepSelectorDialogPaneLocationXY,9999,9999`
Step Selector Dialog Window Control	`StepSelectorDialogPaneWidth,720 (existing RunParm)`
Step Selector Dialog Window Control	`StepSelectorDialogPaneHeight,440 (existing RunParm)`

* NOTE: RunParm ProofAsstFormulaRightCol sets the right margin for TMFF (Text Mode Formula Formatting) in the Proof Assistant Window, and in the existing code, changes to the size of the Proof Asst GUI window do not affect the TMFF-rendered width of proof formulas. However, as part of Release 20121225 this behavior will change. When the user changes the width of the Proof Assistant GUI window, or chooses a different font, font size, or bold vs. plain, the number of characters that fit inside the borders of the window's "viewport" are affected, plus or minus, and these changes will automatically update the (internally) stored setting for ProofAsstTextColumns. The updated setting will become visible during the next TMFF proof formatting operation, and it will be stored as part of the persistent GUI preferences data. Similarly, changes affectingthe height of the Proof Assistant window or the error message area will automatically update the settings for ProofAsstTextRows and ProofAsstErrorMessageRows.

(NEW) SEARCH OPTIONS WINDOW PrevSearchData HISTORY

iTH PREV SEARCH OPTIONS FIELD	GUI PREFERENCES FILE COMMAND
PrevSearch i, OR	`PrevSearch,OR,i,XXXX`
PrevSearch i, QUOTE	`PrevSearch,QUOTE,i,XXXX`
PrevSearch i, Line j, Search-In-What	`PrevSearch,Search-In-What,i,j,XXXXXXXXXXXXXXXX`
PrevSearch i, Line j, Format	`PrevSearch,Format,i,j,XXXXXXXXXXXXXXXX`
PrevSearch i, Line j, Oper	`PrevSearch,Oper,i,j,XXX`
PrevSearch i, Line j, Search-For-What	`PrevSearch,Search-For-What,i,j,XXXXXXXXXXXXXXXXXXXXXXXXXXXXX`
PrevSearch i, Line j, Or	`PrevSearch,Search-For-What,i,j,yes/no`
PrevSearch i, From_Chap	`PrevSearch,From_Chap,i,XXXXXXXXXXXXXXXXXXXXXX`
PrevSearch i, From_Sec	`PrevSearch,From_Sec,i,XXXXXXXXXXXXXXXXXXXXXX`
PrevSearch i, Thru_Chap	`PrevSearch,Thru_Chap,i,XXXXXXXXXXXXXXXXXXXXXX`
PrevSearch i, Thru_Sec	`PrevSearch,Thru_Sec,i,XXXXXXXXXXXXXXXXXXXXXX`
PrevSearch i, Labels	`PrevSearch,Labels,i,XXXXXXXXXXXXXXXXXXXXXX`
PrevSearch i, Min_Times_Used_In_Proofs	`PrevSearch,Min_Times_Used_In_Proofs,i,99999`
PrevSearch i, Min_Hyps	`PrevSearch,Min_Hyps,i,99999`
PrevSearch i, Max_Hyps	`PrevSearch,Max_Hyps,i,99999`
PrevSearch i, Max_Search_Results	`PrevSearch,Max_Search_Results,i,99999`
PrevSearch i, Must_Be_Unifiable_With_Step	`PrevSearch,Must_Be_Unifiable_With_Step,i,yes/no`
PrevSearch i,Use_Chapter_Sec_Hierarchy	`PrevSearch,Use_Chapter_Sec_Hierarchy,i,yes/no`
PrevSearch,i,Search-Proximity_Scoring	`PrevSearch,Search-Proximity_Scoring,i,yes/no`
PrevSearch,i,Min_Completed_Search_Results	`PrevSearch,Min_Completed_Search_Results,i,99999`
PrevSearch,i,Check_First_N_Search_Results	`PrevSearch,Check_First_N_Search_Results,i,99999`
PrevSearch,i,Max_Incomplete_Hyps	`PrevSearch,Max_Incomplete_Hyps,i,99999`
PrevSearch,i,Max_Prev_Steps_Checked	`PrevSearch,Max_Prev_Steps_Checked,i,99999`
PrevSearch,i,Reuse_Derivation_Steps	`PrevSearch,Reuse_Derivation_Steps,i,yes/no`
PrevSearch,i,Max_Elapsed_Seconds	`PrevSearch,Max_Elapsed_Seconds,i,99999`
PrevSearch,i,Show_Unification_Subst	`PrevSearch,Show_Unification_Subst,i,yes/no`
PrevSearch,i,Auto_Select	`PrevSearch,Auto_Select,i,yes/no`
PrevSearch,i,Output_Sort_Seq	`PrevSearch,Output_Sort_Seq,i,XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX`

(NEW) SEARCH OPTIONS WINDOW Search-For-What HISTORY

iTH SEARCH-FOR-WHAT/HISTORY ITEM	GUI PREFERENCES FILE COMMAND
Hist,Search-For-What,CharString,i	`Hist,Search-For-What,CharString,i,XXXXXXXXXXXXXXXXXXXXXXXXXXXXX`
Hist,Search-For-What,ParseExpr,i	`Hist,Search-For-What,ParseExpr,i,XXXXXXXXXXXXXXXXXXXXXXXXXXXXX`
Hist,Search-For-What,ParseStmt,i	`Hist,Search-For-What,ParseStmt,i,XXXXXXXXXXXXXXXXXXXXXXXXXXXXX`
Hist,Search-For-What,RegExpr,i	`Hist,Search-For-What,RegExpr,i,XXXXXXXXXXXXXXXXXXXXXXXXXXXXX`