Topic: paste the goal at the cursor
Johan Commelin (Nov 14 2020 at 08:32):
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
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
Edward Ayers (Nov 15 2020 at 19:27):
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:45):
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):
Last updated: May 14 2021 at 22:15 UTC