Panics in the web editor

Stream: lean4

[Eric Wieser]

Is it possible to see panic messages in the web editor? The following only works in vscode:

#eval (panic "oh no" : Nat)

[Eric Wieser]

(context: lean4#4983, where I wanted to reproduce a panic but couldn't do so in the editor!)

[Jon Eugster]

https://github.com/leanprover-community/lean4web/issues/33

I added an issue :+1:

[Eric Wieser]

Thanks! Did this use to work, or am I thinking of only the "internal panic"s which crash the server?

[Sebastian Ullrich]

This will likely "just work" in 4.12.0 lean#4952

[Jon Eugster]

I vaguely remember that Alex did a manual banner for when the server crashed, which had the same style as the ones in VSCode