Zulip Chat Archive

Stream: general

Topic: can't copy in widget mode

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


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

edit: link to another recent Zulip thread

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

Kenny Lau (Jul 30 2020 at 10:37):


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

Edward Ayers (Jul 30 2020 at 11:08):


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?

Kenny Lau (Aug 03 2020 at 16:26):


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: Aug 03 2023 at 10:10 UTC