Work arounds for using the Mathcal letter?

Stream: Emacs

[Kent Van Vels]

Hi, I guess it is a known issue that the goal-window in emacs doesn't play nice with the calligraphic math letters like

𝓛 𝓝 𝓡

It seems like there is an issue with it missing a trailing space. Is there a work-around for this?

[Yury G. Kudryashov]

Works for me

[Yury G. Kudryashov]

(I tried an example with a type called 𝓡)

[Kevin Buzzard]

I know nothing about Lean in emacs but could this be a font issue rather than an emacs issue?

[Kent Van Vels]

@Yury G. Kudryashov , I am having the problem you mentions in this post #Emacs > Support: Use Emacs for Lean? @ 💬 , I thought it was other mathcal letters too, like the principal filter. I will update my lean4 mode and see if that changes anything.

[Yury G. Kudryashov]

This is a different issue: if a line contains some Unicode characters, then lsp client&server count them as different number of characters, hence the server thinks that you're inserting text at a wrong position.

[Kent Van Vels]

Yeah, that is the issue I am having. I have some luck killing then yanking the lines.

[Kent Van Vels]

For anyone's information, I have been using Emacs inside a terminal (as all good hackers do) today and I think I have been having some luck with this issue.

I am leaving this post here as remind to report more later.

[Yury G. Kudryashov]

@Kent Van Vels Any details?

[Joseph Myers]

The patch at https://github.com/yyoncho/lsp-mode/commit/aac9b6a10611ce9fcb4c9fe272f2835f0b6bb210 (as linked from https://github.com/emacs-lsp/lsp-mode/issues/2080 ) works for me (at least once I deleted the lsp-mode.elc that had been byte-compiled before I patched lsp-mode.el). Though if some version of https://github.com/leanprover/lean4/pull/2646 got into Lean then that might avoid the lsp-mode issue by allowing the use of UTF-32 LSP.

[Yury G. Kudryashov]

I'll try to figure out how to apply a patch to lsp-mode in NixOS tomorrow.

[Yury G. Kudryashov]

Thanks for the link!

[Kent Van Vels]

@Yury G. Kudryashov, it still had the same problems. The letters were truly monospace though.

[Mekeor Melire]

Related quote from this message: #Emacs > Development: Maintainership @ 💬

Eglot has one key advantage over lsp-mode: it correctly handles LSP's weird specification of source positions, where column numbers have to be in terms of 16-bit Unicode. lsp-mode still doesn't[.]

[Yury G. Kudryashov]

Note: the patch worked.

[Yury G. Kudryashov]

I'm OK with switching from lsp-mode to Eglot if we can figure out how to get syntax highlighting work.

[Mekeor Melire]

The plan is to support both lsp-mode as well as Eglot. Both have their up- and downsides respectively.

As far as I know, no one is currently actively working on making Eglot support semantic tokens. There are one or two third-party packages that extend Eglot with this intention, but I haven't tried them out yet.