show_panel_widgets command

def Lean.Widget.widgetInstanceSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.addWidgetSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.eraseWidgetSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Widget.showWidgetSpec : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

#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.

Equations

• Lean.Widget.widgetCmd = Lean.ParserDescr.node `Lean.Widget.widgetCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#widget ") Lean.Widget.widgetInstanceSpec)

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

Equations

• One or more equations did not get rendered due to their size.