copy messages in VSCode

Stream: general

[Floris van Doorn]

• In recent versions of VSCode I cannot copy messages (tactic states, trace messages, error messages) from the Lean infoview anymore. If I select text and press ctrl+V (or right-click it), nothing happens for me. Is this a recent change? Is this because of widgets? Or is it a bug?
• Sometimes the copy message to comment button doesn't work for me anymore. I cannot reproduce how this happens, but it happened more than once. Closing+reopening VSCode fixes it (so far).

[Kevin Buzzard]

You switch back to old mode in the drop down menu and then copy that instead

[Gabriel Ebner]

This is definitely not intentional. And it works just fine for me. (I can copy the tactic state by just selecting it, or by pressing ctrl+c.) What operating system are you on?

[Eric Wieser]

I'm seeing the same thing on windows. If I try over and over again, I can eventually get the state to copy.

[Eric Wieser]

I assume this is the dropdown Kevin refers to: image.png

[Eric Wieser]

Here's what I see happen when I try to copy:

1. I click on a word I want to copy
2. The widget box appears
3. I make the second click of my double-click
4. The selection of the full word appears
5. Almost immediately, the widget box disappears, and my selection along with it

[Gabriel Ebner]

Double-clicking on a word doesn't work for me either. But I don't see how that should work if a single click already opens a popup.
I can select text (by "dragging the cursor over it") just fine. Does that work for you?

[Bryan Gin-ge Chen]

Possibly related VS Code issue: https://github.com/microsoft/vscode/issues/103325

Another thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/can't.20copy.20in.20widget.20mode