Open Alizter opened 9 months ago
Thanks to @Alizter for bringing this issue to my attention, a couple of comments:
lean4-vscode
does it is a good referenceGoalsAnswer<String>
provided in the view would be trivial, so the copy button could call that function before copying indeed (and even query the open/close status of some UI items)
This issue is a collection of related issues about copying.
The only way to copy selected text in the window is using Ctrl+C. Together with vim mode, this can be inconvenient. I think having a copy button would be useful.
The structural parts of the goal window cannot be selected. Things like the hypothesis colons, proof bar etc.
The right click copy menu is useless.