## Stream: general

### Topic: can't copy in widget mode

#### Kenny Lau (Jul 26 2020 at 17:34):

#mwe:

#check 0 -- [try copying here]


I can't copy the result from the widget mode by selecting the text, i.e. 0 : ℕ, from either "Messages" or "All Messages". Instead, the whole line (#check 0 -- [try copying here]) is copied, as if my cursor were still in the Lean file.

However, @Chris Hughes tells me that he can copy it for some reason.

#### Kevin Buzzard (Jul 26 2020 at 17:40):

Switch back to non-widget mode for a workaround (there's a drop-down menu to do this).

#### Bryan Gin-ge Chen (Jul 26 2020 at 17:43):

Could it be this VS Code issue? https://github.com/microsoft/vscode/issues/103325 See if trying the "Insiders" version fixes things.

#### Edward Ayers (Jul 30 2020 at 10:37):

I can also copy it fine, both with the 'copy to comment' button and by selecting and doing ctrl+C. What OS are you using? I'm on linux

windows

#### Kenny Lau (Jul 30 2020 at 10:38):

I think sometimes it works fine, sometimes it doesn't

#### Edward Ayers (Jul 30 2020 at 10:39):

does copy to comment always work or does that sometimes fail?

#### Kenny Lau (Jul 30 2020 at 10:39):

oh I've never tried it

#### Kenny Lau (Jul 30 2020 at 10:39):

in fact I was only aware of its existence 2 minutes ago

#3633

#### Kenny Lau (Aug 01 2020 at 12:45):

@Bryan Gin-ge Chen @Edward Ayers I have discovered that I can only copy the output in widget mode if and only if the linebreak after the output is also included

#### Kenny Lau (Aug 01 2020 at 12:46):

either by double-clicking the last line or by manually copying the linebreak by dragging the mouse to a specific region in the space below the line

#### Kenny Lau (Aug 01 2020 at 12:46):

(too left and you won't copy the linebreak)

#### Edward Ayers (Aug 03 2020 at 16:12):

Does the new copy button work on the widget-mode tooltip in mathlib?

yeah

#### Edward Ayers (Aug 04 2020 at 16:52):

Ok hopefully the copy button covers at least some of the use case for copying code from the infoview.

#### Patrick Massot (Aug 04 2020 at 21:58):

Thanks a lot @Edward Ayers ! It works great, except when the button is so far to the right that it leaves my screen.

Last updated: May 17 2021 at 23:14 UTC