See result without moving cursor to `#eval`

Stream: new members

[Iocta]

#eval [1, 2, 3, 4, 6, 8, 9, 10, 15] |>
  map (fun x => 10 * x) |>
  map (fun x => x + 1) |>
  map (fun x => x - 1)

In VSCode, each time I add a line to the end of this pipeline, I have to move my cursor up to #eval at the top in order to see the result. Is there a macro I can use to can see the result with my cursor at the bottom, so I don't have to keep jumping back and forth?

[Eric Wieser]

You can expand the "all messages" window in the infoview

[Sebastian Ullrich]

It should be feasible to do the right thing by default here as well, do consider opening an issue in lean4

[llllvvuu]

It looks fine to me:

Screenshot 2025-02-26 at 5.46.25 PM.png

[Wang Jingting]

try the "error lens" extension on VS code! The result looks something like @llllvvuu 's screenshot.