Showing a panel widget globally

[Vtec234]

Currently, the only supported ways to display a panel widget are to

• use the withPanelWidgets tactic combinator; or
• use the #widget command; or
• use the lower-level savePanelWidgetInfo function.

Under the hood, all of these associate a panel widget with a particular syntactic span by storing an ofUserWidgetInfo node in the infotree. Unfortunately, this cannot work for choosing to display a widget globally, i.e. to always display it regardless of where in the file the cursor is. This is because infotrees are command-local, so cannot span more than one command by design. To support a command show_panel_widgets [MyDisplay] which enables MyDisplay globally, it seems an environment extension has to be added to Lean core and queried in getWidgets.