Zulip Chat Archive

Stream: general

Topic: copy messages in VSCode


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

view this post on Zulip Kevin Buzzard (Jul 23 2020 at 23:06):

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

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

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

view this post on Zulip Eric Wieser (Jul 24 2020 at 12:05):

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2020 at 17:44):

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

Another thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/can't.20copy.20in.20widget.20mode


Last updated: May 10 2021 at 00:31 UTC