RFC: Copy paste hover highlighted "selection" from infoview.

Stream: lean4

[Moritz R]

When you hover a term in the infoview, it shows you nicely via a blue background (which is not a cursor selection, but looks alot like it!) what the boundaries of the term are.

It would be really nice if we could just press Ctrl/Cmd+c to copy this current hightlighted part (instead of really selecting the part with the cursor and then pressing Ctrl/Cmd+c)

Is there maybe an extension capable of doing this that i don't know?

[Marc Huisinga]

When you right click a highlighted term, it is selected, so using "Copy" from the context menu on it will copy the highlighted term.

We may also be able to override the copy event handler of the webview in cases where there is no text selected but there is a highlighted term to make Ctrl+C work.

[Thomas Murrills]

Hmm, this doesn't seem to work for me. Right-clicking while hovering over a non-selected but highlighted term, then clicking copy, copies the whole line; this is consistent with what I see during right click (no highlighting or selection, just my cursor in the spot I right-clicked). (I'm on macOS if relevant.)

[Moritz R]

I just tested this on a windows machine:
hovering -> right click -> select "copy" always works as expected.

hovering -> right click -> Ctrl+c either doesn't work at all (doesnt change the clipboard) or copies the whole line or sometimes a different full line (even though the pop up menu has Ctrl+c as a shortcut next to the copy option!

hovering -> Ctrl+c also either doesn't work at all (doesnt change the clipboard) or copies the whole line or sometimes a different full line.

[Moritz R]

Interestingly the copy command from the vscode command palette doesn't work at all with any combination of things i tried.

[Moritz R]

On my mac machine, interestingly
hovering -> right click -> select "copy" also always works as expected.

hovering -> right click -> Cmd+c always works as expected?!

hovering -> Cmd+c never works, maybe it's a infoview-focus problem?

[Moritz R]

Interestingly the copy command from the vscode command palette sometimes seems to work if i right click after hovering

[Moritz R]

(deleted)

[Marc Huisinga]

The context menu and the copy functionality are handled by VS Code, not Lean or the Lean VS Code extension.

[Moritz R]

We could certainly provide a command-palette action to copy the hovered text and also a "when" condition like infoviewTextHovered, so that we can override ctrl+c in these situtations using a vscode keybinding?

[Marc Huisinga]

You also need to ensure that the InfoView is focused, because otherwise Ctrl+C can copy text e.g. from your editor if text is already selected there. I'd prefer trying to just override the webview copy event instead of adding more VS Code command <-> webview communication.

[Marc Huisinga]

(The focus issue is why every solution here will be somewhat unintuitive to users because you can always hover over terms in the InfoView without focusing it)

[Moritz R]

ideally the copying would work, even without infoview focus? That's why i didn't include it in infoviewTextHovered

[Moritz R]

A custom command palette action could work without needing focus on the infoview

[Marc Huisinga]

What text do you copy if there is text selected in the editor or some other panel that is currently focused? What happens when you've focused the terminal and are running a command that should be cancelled by Ctrl+C?

[Moritz R]

In my opinion we should prefer copying the infoview hovered text in all these scenarios.

[Moritz R]

For the terminal we can add a !terminalfocused though

[Marc Huisinga]

Let's not change how standard VS Code operations behave w.r.t. focusing - I expect that this will result in even more confusing behavior than the alternative (e.g. your mouse is in the InfoView, you start typing, your mouse is hovering over a subterm by accident, you hit Ctrl+C to copy text in your editor and it unexpectedly copies text from the InfoView instead).