Links in messages?

Stream: lean4

[Mario Carneiro]

Is it possible to create a MessageData containing a link (which calls a server RPC method)? Widgets can do this, but I haven't figured out how to make rich message objects containing interactable things except by embedding Expr and getting Expr tooltip stuff.

[Wojciech Nawrocki]

Not yet, but a mechanism is proposed in lean4#2064

[Mario Carneiro]

aha, example 1 looks similar to what I'm working on :wink:

[Mario Carneiro]

I have also wanted to do better hyperlinks in the output of #help, rather than putting references to the actual expr constants with weird names