Zulip Chat Archive

Stream: general

Topic: widget copy


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

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

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

view this post on Zulip Patrick Massot (Jul 02 2020 at 13:43):

We've been waiting for this button for soo long.

view this post on Zulip Edward Ayers (Jul 02 2020 at 13:46):

Should be possible with the next release of lean...

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 20:41):

Mjolnir button.

view this post on Zulip 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 a suffices : ..., by simpa. The button could create those lines and, probably harder to get reliably, remove the simp call.

This could be implemented by having a tactic suffsimp that is an alias of simp but outputs some Try this: message.

view this post on Zulip Johan Commelin (Jul 02 2020 at 20:47):

But of course, implementing it via widgets is cleaner.

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

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

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 21:12):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 21:13):

Oh, I missed Johan's message.

view this post on Zulip Edward Ayers (Jul 06 2020 at 14:33):

this can now be implemented in mathlib!


Last updated: May 17 2021 at 21:12 UTC