Ed Ayers

Another extension I use is having a similar crisis: https://github.com/paradoxxxzero/gnome-shell-system-monitor-applet/issues/672 https://github.com/paradoxxxzero/gnome-shell-system-monitor-applet/pull/678

Also true for all other kinds of binder. I think the problem is in `withBindingBodyUnusedName` in `src/lean/prettyprinter/delaborator/basic.lean`. We are annotating the `i` with the subexpr position of the parent expression....

I tried to reproduce again on this file and I can't, it all seems to be working now. I'll keep developing and see if I can catch it failing again....

keen for this outside of vim mode too

yes this is exactly a use case of the user-widgets feature

I sometimes have to wait about 5 seconds with no visual feedback before the item disappears from the list. Perhaps this is the same bug.

this is useful outside of vim too

Hi I was the one who added tachyons. It's a divisive library. As Gabriel says it was mainly to save some headaches on the widgets stuff, however Lean 4 widgets...

I really like tachyons tbc.

It would make things harder for us if it was removed now, but we can go forward working with the assumption that the library will be gone one day and...