"Try this" replaces incorrect segment about lean.nvim HOT 6 CLOSED

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?

from lean.nvim.

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

from lean.nvim.

This is what I see here:

Will need some way of reproducing the broken behavior I think

from lean.nvim.

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.

from lean.nvim.

I was using trythis, and I have gotten it to work with code action now :) Thanks a lot!

from lean.nvim.

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.

from lean.nvim.