can't copy in widget mode

Stream: general

[Kenny Lau]

#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]

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

[Bryan Gin-ge Chen]

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

edit: link to another recent Zulip thread

[Edward Ayers]

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

[Kenny Lau]

windows

[Kenny Lau]

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

[Edward Ayers]

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

[Kenny Lau]

oh I've never tried it

[Kenny Lau]

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

[Edward Ayers]

#3633

[Kenny Lau]

@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]

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]

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

[Edward Ayers]

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

[Kenny Lau]

yeah

[Edward Ayers]

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

[Patrick Massot]

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