## Stream: general

### Topic: paste the goal at the cursor

#### 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

#### 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

#### Johan Commelin (Nov 14 2020 at 09:35):

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

#### 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:

#### 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

Hi

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

#### Edward Ayers (Nov 15 2020 at 19:31):

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

#### 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.

#### Edward Ayers (Nov 15 2020 at 22:01):

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

#### Bryan Gin-ge Chen (Nov 15 2020 at 22:04):

I think absolute position might end up easier.

#### 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

#### Kevin Buzzard (Nov 15 2020 at 23:01):

Thanks Ed!

Last updated: May 14 2021 at 22:15 UTC