InfoView selection UX

Stream: lean4

[Patrick Massot]

My teaching library uses the possibility to select things in the InfoView using Shift-click in VSCode. I noticed while watching new users that this workflow is rather confusing because the difference with regular “highlighting selection” is not clear. Would it be possible to prevent regular selection? It probably cannot be a permanent things because people use regular selection to copy-paste from the infoView (especially since the copy-paste menu is broken). But ideally widgets could disable it (or at least there would be an extension settings). @Marc Huisinga

[Mario Carneiro]

I don't think widgets should disable manual copy-paste

[Patrick Massot]

What do you propose then?

[Mario Carneiro]

I don't really have a proposal, but perhaps just plain clicking with some button-like effect on the selectable options?

[Patrick Massot]

I’m sorry, I have no idea what you mean.

[Patrick Massot]

What do you call “the selectable options”?

[Mario Carneiro]

the hypotheses, in your case?

[Mario Carneiro]

I'm not really sure what is selectable for your widget

[Patrick Massot]

A priori everything is selectable. And this is really not specific to my teaching widget. The current interface is confusing for everything that relies on shift-click selection.

[Mario Carneiro]

I'm saying that the issue is using shift-click for selection, this is really non-discoverable

[Mario Carneiro]

maybe throw up a banner saying "shift-click to select" when a widget is doing something with this

[Mario Carneiro]

if you use click to select I think that is more natural / discoverable although it is better with a button effect

[Mario Carneiro]

re: "a priori everything is selectable", perhaps so but not all widgets are doing things with all possible selectable items at all times

[Mario Carneiro]

most of the time shift-click does nothing and (even assuming people think to try it) people will get used to this and be thrown off when that's not the case

[Patrick Massot]

Oh I agree with this.

[Patrick Massot]

The widgets that use this mechanism say it, but this is clearly not enough.

[Patrick Massot]

I could try to use a bigger message, but this would not fix the issue that things that are selected by shift-click are very hard to distinguish from things that are selected as text.

[Patrick Massot]

Also keep in mind that several things can be shift-clicked (and this is crucial for my use case).

[Mario Carneiro]

I think the message should go before the goal view, not in the widget area

[Mario Carneiro]

for selecting multiple things without deselecting everything else I agree shift-click or ctrl-click is a good choice. People have probably seen this pattern elsewhere, for example selecting files in windows explorer

[Patrick Massot]

Except they expect Ctrl-click while Ctrl-click does something completely different.

[Mario Carneiro]

then maybe that's the first place to look for improvements...?