Copy paste from infoview in VSCode on windows

Stream: new members

[Ryan McCorvie]

I don't have a full #mwe, but I thought I would ask about this in case its a common known issue.

The quote marks icon in the infoview which does a "copy paste" to to a comment in the buffer does not always copy correctly. It will generate a comment in my buffer, but sometimes he body of the comment is empty, or contains just some of characters from the message I'm trying to copy. If I look at the windows-v clipboard history, I can see the desired text is not on the system clipboard, so I think the problem is with the "copy" not the "paste".

I have had the same message not copy, and then later in a new session it will copy, so I don't thik it's a deterministic problem related to the text being copied. I had a notion that it might be related to the specific unicode characters being copied, but I haven't been able to find any pattern so far.

Sometimes only part of the text gets copied. From my current session:
#eval foo gives unkown identifier: 'foo' in the infoview but only unknown idenfitier '' in the copied comment block. Similarly when I
copy the results of a #print @myfunction in my current session it only copies the : of the function definition.

Details about the system:

• Windows 11 Pro (22H2)
• VSCode version 1.78.1
• Lean (version 4.0.0-nightly-2023-03-14, commit 96aa021007cf, Release)
• elan 1.4.2 (4a1b1b918 2022-09-13)

I can provide screenshots of my systems settings for copy/paste for the OS and VSCode if its useful, I didn't see any smoking guns there.

[Kyle Miller]

Thanks for mentioning it -- I think many of us individually know about this issue, but I'm not sure if it's come up on the Zulip yet.

It'd definitely an annoying bug. What I usually do to work around it is select the text I want to copy myself.

[Kyle Miller]

My guess has been it has to do with how MessageData is displayed in VS Code, but that's just speculation. The string parts of MessageData seem to always copy correctly, but then embedded expressions don't seem to copy.

[Ryan McCorvie]

@Kyle Miller Thanks for that suggestion. What mechanism do you use to copy? When I right-click copy from the infoview it also fails to work for me sometimes. I don't see the text copied onto the clipboard history. I also sometimes have problems right-click copying text from the HTML pane where I am reading TPIL, so maybe its not an infoview problem.

[Kyle Miller]

I think I do Ctrl-C after selecting

[Wojciech Nawrocki]

Hi, this is vscode-lean4#271 . I bumped it to high priority so that either I or someone eventually gets around to fixing it.