1. Enhancements to the Step Selector Search feature to accomplish the following goals:

• Improve the quality of the Step Selector Search results. Objectively speaking, this means that assertion the user wants will appear higher up in the search results than in the current system...statistically speaking.
  
• Provide a general search facility for Metamath assertions which is useful to both mmj2 users and metamath.exe users. Even the most hardcore metamath.exe users will want to keep a parallel mmj2 session running just to perform mmj2 searches.
  
• Provide a Search Options dialog for entry of all search-related preferences and parameters. Specifically, these will enable mmj2 Proof Assistant users to tailor the search criteria for a designated proof step; to perform general ("global") searches not tied to a specific theorem/proof step; and to refine a search using its result set as the input search domain for the next search.
  
• Provide an "Extended Search" feature that will seek to supply missing hypotheses for unifiable assertions in the search results list using previous steps in the Proof Worksheet and/or assertions in the database requiring zero hypotheses.
  
• Provide an "Auto-Select" option to the Step Selector Search that automatically selects the first search result item that fulfills the user's search criteria and which logically completes the designated proof step; it then automatically updates the Proof Worksheet and continues the Unification process.
  
• Modify the Step Selector Search dialog to visually indicate or highlight search result items that fulfill the user's search criteria and logically complete the designated proof step. Regrettably, the current dialog output format does not distinguish these search results from the rest. In addition, the output display sort sequence should, unless the user specifies otherwise, position these search result items at the beginning of the list!
  

2. Provide persistent storage of mmj2 GUI preferences.

3. Changes to the Proof Assistant GUI (main) window

1. Do not attempt cursor positioning for distinct variable errors.
2. Revise the documentation in mmj2/doc/IncompleteStepCursorPositioning.html to indicate that option "AsIs" means the cursor will remain on the same proof step -- not that the row/column position of the cursor will be unchanged.
   
3. Modify RunParm "ProofAsstUnifySearchExclude" to use the "*" statement label wildcard symbol (meaning that 0 or more of any characters in this position is a match), which Metamath.exe uses in the MINIMIZE_WITH command: "MINIMIZE_WITH * /BRIEF /EXCLUDE 3*,*OLD,ee*".
4. Remove Unify menu options Set Step Selector Max Results and Set Step Selector Show Substitutions -- these options will be entered on the new Search Options window.
5. Retain the Unify menu and right-mouse menu item Step Selector Search but add Reuse Step Selector Search and Search Options to these menus. The original choice, Step Selector Search, will initiate a new search using no search data criteria and the current search preferences on the Search Options window; Reuse Step Selector Search will initiate a search using the existing search data criteria and search preferences; and the Search Options choice will display the Search Options window. The first two choices initiate proof-step specific searches while the last choice can be proof-step specific or "global" depending on whether the cursor was positioned on a derivation proof step when the choice was made.
   
6. Dragging (adjusting) the right border on the Proof Assistant GUI window will automatically update the ProofAsstFormulaRightCol which sets the (TMFF) proof formatting right margin. The adjusted setting will be retained for future use via the Persistent Storage Of GUI Preferences enhancement. In the existing code changing the size of the Proof Assistant window has no affect on proof formatting, but with this fix every factor related to the size of proof text (font, font size, bold/plain), and the size of the window will be stored in "persistent storage" so that once the user gets the Proof Assistant screen adjusted to perfection the settings are retained permanently.
   

4. Changes to the Step Selector Search Dialog window

1. The "Hide Dialog" button will be replaced with two new buttons: "Goto Proof Asst." and "Goto Search Options". This change provides accessibility to the other two key Proof Assistant windows in the situation where the user has positioned the windows so that they overlap, partly or completely. The "Goto xxxx" action simply puts the destination window on top -- it does not hide or minimize the original (source) window. In the situation where the user has a small screen, like a tablet, this behavior is important. In a different situation where the user has a large screen capable of displaying all of the windows simultaneously, the user can simply "mouse" or "alt-tab" to the desired window (to give it the input focus.)
2. The characters "(!!!)" will be displayed prefixing the label of each search result item that satisfies the user search criteria and logically completes the designated proof step. These search results will appear at the beginning of the list (unless an alternative output sort sequence is requested on the Search Options window -- though at this time every possible sort sequence has Score as the major sort key, so these search results will appear first in every case, assuming any exist.)
   
3. The characters "(---)" will be displayed prefixing the label of each search result item that fails to satisfy the user search criteria and is present in the search results only because Search Proximity Scoring was requested. These search results will appear at the end of the list (unless an alternative output sort sequence is requested on the Search Options window -- though at this time every possible sort sequence has Score as the major sort key, so these search results will appear last in every case, assuming any exist.)
4. The descriptive Metamath Comment for each search result item's assertion will be displayed if the search criteria included a search of Metamath Comments. The Comment data will be displayed as a 3rd line of text following the conclusion line of the search result.