Closed grhkm21 closed 9 months ago
This seems to work correctly here (now?). I'm on Lean 4.3.0rc1, Mathlib4 df32aa2ebe0f1ef9bce7831b1bcc0723f07a4724 and NVIM v0.9.4. Can you confirm whether it does or doesn't for you?
Hi, sorry for the late reply. No, it doesn't work for me. I'm on NVIM v0.9.4, Lean v4.3.0-rc1, Mathlib b6ec7450650a5945bf4244751be4a5cf1fee962f. It's very interesting that it works for you, my understanding is it shouldn't...
Also, I think I have a fix idea, but I haven't gotten to implement it yet. Essentially, we should implement the .getWidgets
RPC (found here) and use those directly to get the replacement range (and the js widget source code, which we ignore for now).
This is what I see here:
https://github.com/Julian/lean.nvim/assets/329822/eee22758-68e5-4579-81c0-edf03b38528b
Will need some way of reproducing the broken behavior I think
To be sure -- are you using lean.trythis.swap
or the code action here? You should be using the latter on Lean 4, given it exists now.
I was using trythis, and I have gotten it to work with code action now :) Thanks a lot!
Cool, ok glad it works, I'll try to make this clearer -- I'd already removed lean.trythis
from the readme but I think the next step would be not binding it at all in Lean 4 buffers, which should send a message at least. I'll likely do that and then close this. Thanks regardless for the issue.
Hi. Here's code:
With this code, it is supposed to change the entire line, as specified by
![Screenshot 2023-10-19 at 21 20 25](https://github.com/Julian/lean.nvim/assets/83517584/49c08d13-f4a2-4238-a476-5d8cc06325a8)
origSpan?
. Apparently it does on VSCode c.f. Mario. However, the plugin doesn't - it replaces it withf 3 = 4 a b c d e f g
.