Topic: copy messages in VSCode
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 commentbutton 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).
Kevin Buzzard (Jul 23 2020 at 23:06):
You switch back to old mode in the drop down menu and then copy that instead
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?
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.
Eric Wieser (Jul 24 2020 at 12:05):
I assume this is the dropdown Kevin refers to: image.png
Eric Wieser (Jul 24 2020 at 12:07):
Here's what I see happen when I try to copy:
- I click on a word I want to copy
- The widget box appears
- I make the second click of my double-click
- The selection of the full word appears
- Almost immediately, the widget box disappears, and my selection along with it
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?
Bryan Gin-ge Chen (Jul 26 2020 at 17:44):
Possibly related VS Code issue: https://github.com/microsoft/vscode/issues/103325
Last updated: May 10 2021 at 00:31 UTC