Zulip Chat Archive

Stream: general

Topic: can't copy in widget mode


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 30 2020 at 10:37):

windows

view this post on Zulip Kenny Lau (Jul 30 2020 at 10:38):

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

view this post on Zulip Edward Ayers (Jul 30 2020 at 10:39):

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

view this post on Zulip Kenny Lau (Jul 30 2020 at 10:39):

oh I've never tried it

view this post on Zulip Kenny Lau (Jul 30 2020 at 10:39):

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

view this post on Zulip Edward Ayers (Jul 30 2020 at 11:08):

#3633

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 01 2020 at 12:46):

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

view this post on Zulip Edward Ayers (Aug 03 2020 at 16:12):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 16:26):

yeah

view this post on Zulip 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.

view this post on Zulip 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