Zulip Chat Archive

Stream: general

Topic: paste the goal at the cursor


view this post on Zulip Johan Commelin (Nov 14 2020 at 08:32):

The Try this stuff is really awesome, and the Alt-V shortcurt in VScode makes it even better. How hard is it to add a keyboard shortcut that pastes the content of the first goal ar the cursor?
That would be useful for writing change statements or calc blocks

view this post on Zulip Alex Peattie (Nov 14 2020 at 09:24):

It shouldn't be hard I think :smile:. There's already Lean: Info View: Copy Contents to Comment (no keyboard binding). I think a naive approach of just taking that same output, finding the first line starting with and pasting it at the cursor ought to work

view this post on Zulip Johan Commelin (Nov 14 2020 at 09:35):

I have no experience at all with vscode extensions or typescript... :sad:

view this post on Zulip Alex Peattie (Nov 14 2020 at 09:36):

I'm happy to take a crack at it next week if no-one else gets there first :thumbs_up:

view this post on Zulip Bryan Gin-ge Chen (Nov 14 2020 at 16:32):

I started working on this, but it's a little tricky because the current infoview API only knows how to insert text at the line above the cursor position. See this hack.

Here's what I have so far. I think it gets the correct goal text, but as mentioned it puts it at the wrong position. I can try to figure out how to paste at the cursor instead, but any suggestions on how best to do this without adding even more layers of hacks would be welcome.

Also, while playing around with this, I came up with a related feature request: in the widget view, I'd like to be able to click on a hypothesis name or the goal symbol (these currently are unlinked) and have the extension copy the hypothesis or goal to the clipboard. We can currently sort of do this by clicking on the head symbol of the expression and clicking the copy-to-clipboard button in the widget popup, but finding the right symbol to hover over can be fiddly.

cc: @Edward Ayers

view this post on Zulip Edward Ayers (Nov 15 2020 at 19:27):

Hi

view this post on Zulip Edward Ayers (Nov 15 2020 at 19:30):

It should be ok for me to add an argument to the effect.insert_text thing so that you can insert text at any point in the doc (perhaps relative to cursor position?)

view this post on Zulip Edward Ayers (Nov 15 2020 at 19:31):

I think that the second related feature request can be implemented in mathlib

view this post on Zulip Bryan Gin-ge Chen (Nov 15 2020 at 20:09):

Hey Ed, sounds good. Let me know how you want to proceed. No rush, of course, if you're busy.

view this post on Zulip Edward Ayers (Nov 15 2020 at 22:01):

Wrt the inserting thing, do you need relative position or absolute position from the cursor?

view this post on Zulip Bryan Gin-ge Chen (Nov 15 2020 at 22:04):

I think absolute position might end up easier.

view this post on Zulip Edward Ayers (Nov 15 2020 at 22:45):

https://github.com/leanprover-community/lean/pull/501
https://github.com/leanprover/vscode-lean/pull/234

view this post on Zulip Edward Ayers (Nov 15 2020 at 22:46):

widget.effect.insert_text now takes an extra arg expecting the relative or absolute position to insert the text at

view this post on Zulip Kevin Buzzard (Nov 15 2020 at 23:01):

Thanks Ed!


Last updated: May 14 2021 at 22:15 UTC