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.
_______________________________________________
Devel mailing list
Devel@lists.geany.org
https://lists.geany.org/cgi-bin/mailman/listinfo/devel
