Writing messages to Lean Infoview?

Stream: Is there code for X?

[Herman Chau]

I'm interested in writing a package that will parse and display the nearest comment to the user's cursor in LaTeX inside the infoview. I've tried is implementing a widget but the custom widget only displays when the user's cursor is on the #widget line. I also see the Message class here https://github.com/leanprover/lean4/blob/82401938cfe99f4a12195aa18a076b27399e20ae/src/Lean/Message.lean#L6 but don't know how I would go about creating and displaying an instance of the class.

Could someone point me to some resources for how I might go about displaying custom messages to the infoview?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Have you seen docs4#Lean.Widget.showPanelWidgetsCmd ? You can put it at the top of the file, and your widget will be shown throughout.

[Herman Chau]

This looks like what I'm looking for. I'll give it a try, thanks!