paste the goal at the cursor

Stream: general

[Johan Commelin]

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

[Alex Peattie]

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

[Johan Commelin]

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

[Alex Peattie]

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

[Bryan Gin-ge Chen]

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

[Edward Ayers]

Hi

[Edward Ayers]

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?)

[Edward Ayers]

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

[Bryan Gin-ge Chen]

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

[Edward Ayers]

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

[Bryan Gin-ge Chen]

I think absolute position might end up easier.

[Edward Ayers]

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

[Edward Ayers]

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

[Kevin Buzzard]

Thanks Ed!