Bug Fix: Incomplete Step Curror Positioning, AsIs Mode

Problem: Viewport always scrolling to the cursor position, which is set to line 1.

See mmj2jar\myproofs\CursorTest.mmp

Three complicating factors are involved. They affect the problem as well as the perception of the problem:

1. The Proof Assistant GUI regards as a step as a validly "Incomplete Step" (with respect to cursor positioning) only when it is a Derivation Step with

a "?" between the 1st and 2nd colons of the Step:Hyp:Ref field. or
the formula contains a Work Variable (e.g. "&C1, "&S1", "&W1", etc.)

A proof step which isn't Incomplete and fails unification (including the attempted Unification Search lookup of Ref for the statement) is considered to be "in error". From the user's perspective a step is "incomplete" whereas mmj2 considers it to be in error. For example, Step 2 below is "in error" after unification, not Incomplete:

   
2::         |- x = x

During proof development it may be more efficient to code place-holder steps, (if needed), like this:

   
3:?:        |- x = x



Or,

   
3:?:        |- &W1

Or, simply:

    3:: 
       |- &W1

2. The existing "AsIs" code in the processing of Incomplete proof steps does replace the current cursor with the saved input cursor, but the code does so even if the cursor has earler been set in the Proof Assistant unification process.

3. The Java RunTimeEnvironment system (JRE) has default processing -- which mmj2 is using -- related to cursor positioning involving a JViewPort. Specifically, the JViewPort is automatically scrolled by the JRE in order to ensure that the Cursor is visible withing the View Port rectangle. If this default scrolling process is not triggered by the mmj2's selected cursor position, then the Proof Assistant can choose to either trigger the scrolling behavior (to match cursor position), or not. Prior to this code fix, the Proof Assistant always triggered the scrolling behavior during the Incomplete Step Cursor Positioning.

Solution: (New Post-Unification Cursor Positioning / Scrolling Logic)

1. After Unification, if the cursor has already been positioned, (i.e. errors found) simply exit cursor positioning routine -- do nothing.

2. If a Metamath proof (RPN) was generated, position the cursor to the 'qed' step and explicitly scroll the viewport to the cursor position. Then exit cursor positioning routine.

3. Set a switch ("dontScroll") in the mmj2 Cursor object so that (just) the next time the proof text is displayed, the mmj2 cursor/scoll rendering logic does NOT explicitly trigger scrolling of the View Port (but the Jave environment may scroll the view in order to keep the cursor visible).

4. Position the cursor according to the "IncompleteStepCursor" Edit Menu option (set via the "ProofAsstIncompleteStepCursor" RunParm.), "AsIs", "Last", or "First":

"Last" or "First" = position the cursor to the last, or first, respectively, Incomplete proof step, if one exists; otherwise, set it to the 'qed' step. The "Ref" field is the standard location within a proof step.
"AsIs" = Restore the saved input Cursor object to the current Cursor object (i.e. cursor position will be unchanged).

NOTE: AsIs is the new default setting for the "ProofAsstIncompleteStepCursor" RunParm -- the old default setting was "Last".