Emacs mode: how to make it use the echo area instead of over

Stream: new members

[Eduardo Ochs]

Hi all! I used Lean for several months in 2023/2024, then stopped, and I am returning now - and the interface of the Emacs mode has changed... the first screenshot below shows the old interface, that was much better for the things that I wanted to do, and the second screenshot shows how things are now.

The new interface shows the current result - (Arith.var "x").mul (Arith.nat 20) : Arith in the screenshot - right justified in the program window, probably using an overlay, and shows only its first line; the old interface showed it in the echo area, and showed multi-line outputs, like trees, correctly.

Is there a way to tell the Emacs mode to show the current result in the echo area instead of showing it as an overlay? How? I couldn't find it, sorry... hints, please?

2024-LuaTreeLean-1.png
sshot.png