In buffer message alignment in lean4-mode

Stream: lean4

[Tomas Skrivan]

The message with #check or #print shows the message aligned to the right and quite often the message does not show fully, see attached picture.

Screenshot-from-2022-05-11-10-52-36.png

I'm not entirely sure if it is problem in lean4-mode, some other part of emacs or my config. Anyway, I was unable to figure out where the problem is. Does this happen to someone else? How can it be fixed?

[Jannis Limperg]

I also have this (also with the Haskell LSP plugin). Don't know what to do about it so I always use the goal buffer.

[Sebastian Ullrich]

Looks like https://github.com/emacs-lsp/lsp-ui#lsp-ui-sideline

[Sebastian Ullrich]

Not exactly much to customize there

[Tomas Skrivan]

Interesting, I increased lsp-ui-sideline-diagnostic-max- line-length/lines and the local context now shows up, neat. But still does not solve the problem with cutting off the end of the line:
Screenshot-from-2022-05-11-11-14-25.png

[Sebastian Ullrich]

Ah, I think this is a problem with Unicode characters, which probably screw up some internal size measurements

[Tomas Skrivan]

Even in C++ it just either cuts off the line or does not show the line at all.

[Sebastian Ullrich]

Note that it is not cut off in your last example, the Y is wrapped to the beginning of the next line

[Tomas Skrivan]

True, but in the first example it is cut off.

[Tomas Skrivan]

Some experimentation in C++:

High line-length
Screenshot-from-2022-05-11-11-25-39.png

Normal line-length, you can see the cut off at ... of type 'const
Screenshot-from-2022-05-11-11-26-05.png

[Tomas Skrivan]

It tries to do some really smart stuff, like find a line where the message fits and display it there. I kind of liked the lean3 behavior where it just add extra lines under #check

[Sebastian Ullrich]

I think that was https://github.com/leanprover/lean-mode/blob/master/lean-message-boxes.el by @David Thrane Christiansen . It shouldn't be too hard to port.

[David Thrane Christiansen]

I'd be happy to explain that code to anyone who needs it, but I don't have time to port it myself right now.

Perhaps it should be generalized into a library that can work with lsp-mode, eglot, or other sources of metadata about a program, and then give it a Lean/LSP backend for this case? It seems like it would be useful for non-LSP data sources as well, like racket-xp-mode, flymake/flycheck, or even M-x compile output.

I can walk you through the design of something like that in my head, and explain the UI code, and generally mentor the elisp development.

[David Thrane Christiansen]

FWIW I don't use lsp-ui at all, and the Lean info buffer is also a reasonable way to see these things for my uses, and it doesn't suffer from the constraints of having to put the messages inline in the buffer text.