feat: shift-click to unselect

[Vtec234]

A simple(istic) implementation of an easier way to unselect hypotheses or types in a goal: shift-clicking anywhere in the info display that "does nothing" (i.e., doesn't select something else or instigate a popup) unselects all items. This might still be a bit annoying, since a shift-misclick will clear everything, but better than nothing. (I am open to suggestions for alternatives.)

Implements context menu entries to (un)select subexpressions in the tactic state, in particular to unselect all of them at once.

CC @PatrickMassot

Screen.Recording.2024-05-22.at.11.25.19.PM.mov

[mhuisi]

Unrelated, but it would also be nice to have a context menu entry for this eventually.

[PatrickMassot]

This is a tricky question. The misclick issue seems pretty serious. Adding a button only for this seems really cluttering. Maybe Marc’s context menu suggestion is a good compromise. It’s not super discoverable but the current proposal is worse from this point of view.

[mhuisi]

LGTM if you're fine with the UX.

[Vtec234]

Following up on the discussion, I implemented the alternative proposal: instead of shift-clicking on the background, unselecting everything is now a context menu option. We can also (un)select specific subexpressions using the context menu.

A remaining usability issue is that when you do this, the type popups still show up (if you have them enabled, but that is the default). Maybe they should be hidden on certain contextmenu events?

Screen.Recording.2025-01-12.at.5.25.06.PM.mov

[mhuisi]

The main two usability issues I've found when testing this PR are that for some reason, when selecting or unselecting a term using the context menu, the term becomes text-selected, and the aforementioned popup. Neither of these are major, so feel free to proceed.

[Vtec234]

(The auto-selection issue is due to #312). I fixed both usability issues by having the tooltip hide on contextmenu, and removing the auto-selection in the new clickedContextMenu handler. More testing is definitely needed, but merging in order to make a pre-release.