Re: Proposal: Only highlight mouse-face when mouse is moved

[Richard Stallman]

    I forgot to explain exactly what it does...:

    1) It keeps track of what the last user activity was:
       - if it was a mouse movement, mouse highlight is enabled
       - if it was a key press, mouse highlight is disabled
       - any other event doesn't change the mouse highlight state

    2) The mouse "sensitivity" is still there.  It is only the
       actual highlighting which is controlled.

    3) This means that the mouse shape still changes to a cross
       when the mouse is over mouse sensitive text.

That seems right to me, except maybe it should also suppress
the change in mouse cursor shape.  I am not sure.