effect insert_text move cursor

Stream: new members

[Angela Li]

Hello! Is there a way for effect.insert_text to move the cursor after the inserted text? I tried reveal_position but I don't think it did anything.
I tried to make clicking for Fifteen (https://github.com/SnobbyDragon/leanfifteen) and it kinda works but you can't see the move unless you click back into the proof.
Thanks!

[Bryan Gin-ge Chen]

I don't think it's possible yet, but https://github.com/leanprover/vscode-lean/pull/234 should make it work. Unfortunately, that depends on lean#501 which also has to be reviewed.

cc: @Edward Ayers (sorry if these pings are getting annoying, Ed!)

[Edward Ayers]

No they are not getting annoying Bryan don't worry!

[Edward Ayers]

Yes for some reason that PR is stalled but it is all in the PR

[Edward Ayers]

I set up a thing that gives a notification whenever someone says widget but it doesn't always work!