show_panel_widgets command

def Lean.Widget.widgetInstanceSpec : ParserDescr

def Lean.Widget.elabWidgetInstanceSpec : TSyntax `Lean.Widget.widgetInstanceSpec → Elab.TermElabM Expr

def Lean.Widget.addWidgetSpec : ParserDescr

def Lean.Widget.eraseWidgetSpec : ParserDescr

def Lean.Widget.showWidgetSpec : ParserDescr

def Lean.Widget.showPanelWidgetsCmd : ParserDescr

Use show_panel_widgets [<widget>] to mark that <widget> should always be displayed, including in downstream modules.

The type of <widget> must implement Widget.ToModule, and the type of <props> must implement Server.RpcEncodable. In particular, <props> : Json works.

Use show_panel_widgets [<widget> with <props>] to specify the <props> that the widget should be given as arguments.

Use show_panel_widgets [local <widget> (with <props>)?] to mark it for display in the current section, namespace, or file only.

Use show_panel_widgets [scoped <widget> (with <props>)?] to mark it for display only when the current namespace is open.

Use show_panel_widgets [-<widget>] to temporarily hide a previously shown widget in the current section, namespace, or file. Note that persistent erasure is not possible, i.e., -<widget> has no effect on downstream modules.

def Lean.Widget.elabShowPanelWidgetsCmd : Elab.Command.CommandElab

#widget command

def Lean.Widget.widgetCmd : ParserDescr

Use #widget <widget> to display a panel widget, and #widget <widget> with <props> to display it with the given props. Useful for debugging widgets.

The type of <widget> must implement Widget.ToModule, and the type of <props> must implement Server.RpcEncodable. In particular, <props> : Json works.

def Lean.Widget.elabWidgetCmd : Elab.Command.CommandElab