Zulip Chat Archive
Stream: general
Topic: widget copy
Patrick Massot (Jul 02 2020 at 13:39):
@Edward Ayers Could we have a small copy button (maybe using the unicode symbol :clipboard:) in a corner of the popup that show up when clicking on a term in the widget? Currently it is harder than before to copy from tactic state because the light blue of term highlighting is hard to distinguish from the dark blue selection highlighting.
Patrick Massot (Jul 02 2020 at 13:41):
Note that I would also enjoy a dedicated button for one of my main use of "copy-paste from tactic state": use simp, copy-paste new goal into a suffices : ..., by simpa. The button could create those lines and, probably harder to get reliably, remove the simp call.
Reid Barton (Jul 02 2020 at 13:42):
Next, a button to call insert extract_goal, extract the output, and automatically post to zulip with topic "code golf"
Patrick Massot (Jul 02 2020 at 13:43):
We've been waiting for this button for soo long.
Edward Ayers (Jul 02 2020 at 13:46):
Should be possible with the next release of lean...
Kevin Buzzard (Jul 02 2020 at 20:41):
Mjolnir button.
Johan Commelin (Jul 02 2020 at 20:47):
Patrick Massot said:
Note that I would also enjoy a dedicated button for one of my main use of "copy-paste from tactic state": use
simp, copy-paste new goal into asuffices : ..., by simpa. The button could create those lines and, probably harder to get reliably, remove thesimpcall.
This could be implemented by having a tactic suffsimp that is an alias of simp but outputs some Try this: message.
Johan Commelin (Jul 02 2020 at 20:47):
But of course, implementing it via widgets is cleaner.
Johan Commelin (Jul 02 2020 at 20:48):
Related question: why do these features require new releases of lean core? I thought that once the main widget functionality was there, we could add new features just in mathlib...
Edward Ayers (Jul 02 2020 at 21:10):
Because in order to get things like copy to clipboard and go to definition to work you need lean to be able to give vscode special commands to do this. Most changes to widgets shouldn't have to wait for a lean update though.
Bryan Gin-ge Chen (Jul 02 2020 at 21:12):
(deleted)
Bryan Gin-ge Chen (Jul 02 2020 at 21:13):
Oh, I missed Johan's message.
Edward Ayers (Jul 06 2020 at 14:33):
this can now be implemented in mathlib!
Last updated: Dec 20 2023 at 11:08 UTC