Dive list: be more careful on when updating the UI after selection

Fix two issues:

1) When narrowing the selection, we didn't get setSelection()
   calls. Only, when the user released the mouse button was
   the selection updated. Therefore, hook into the mouse-release-
   event and update the UI if the selection changed.

2) We updated the ui in setSelection(). However, this was called
   on mouse-move even if the actual selection didn't change.
   Therefore, compare selection before and after processing of
   the event and only refresh the UI if there are changes.

Clearly, this can only be a quick stopgap solution and we
should find out how to properly hook into the selection change
machinery. Though see commit 4928c4ae0421193bbd371cb0924091a970489611
for the reason why we do things as we do them.

Fixes #2595

Reported-by: Willem Ferguson <willemferguson@zoology.up.ac.za>
Signed-off-by: Berthold Stoeger <bstoeger@mail.tuwien.ac.at>

0 files changed, 0 insertions, 0 deletions