## Stream: general

### Topic: copy messages in VSCode

#### Floris van Doorn (Jul 23 2020 at 22:26):

• 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 (Jul 23 2020 at 23:06):

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

#### Gabriel Ebner (Jul 24 2020 at 08:45):

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 (Jul 24 2020 at 12:04):

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 (Jul 24 2020 at 12:05):

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

#### Eric Wieser (Jul 24 2020 at 12:07):

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 (Jul 24 2020 at 12:13):

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 (Jul 26 2020 at 17:44):

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

Last updated: May 10 2021 at 00:31 UTC