I kind of like the idea of selection highlighting being separate highlighting from the search highlighting. That allows you to have multiple groups highlighted differently, which has come in handy in using plugin versions of these features. Alternatively, perhaps we could add having multiple search groups, but that may be more complicated or less intuitive.
On 05/29/2015 07:09 PM, Colomban Wendling wrote:
E.g, have a setting in the preferences "Dynamically mark the current word" that decides whether mark all is dynamic or not, and have shift+ctrl+m toggle the marking, whether it's dynamic or not.