structure ProofWidgets.PanelWidgetProps : Type

• pos : Lean.Lsp.Position

  Cursor position in the file at which the widget is being displayed.

• goals : Array Lean.Widget.InteractiveGoal

  The current tactic-mode goals.

• termGoal? : Option Lean.Widget.InteractiveTermGoal

  The current term-mode goal, if any.

• selectedLocations : Array Lean.SubExpr.GoalsLocation

  Locations currently selected in the goal state.

In the infoview, an info block is a top-level collapsible block corresponding to a given location in a Lean file (e.g. with the header ▼ Basic.lean:12:34).

A panel widget is a component which can appear as a panel inside an info block in the infoview. For example, a tactic state display. The type PanelWidgetProps represents the props passed to a panel widget. The TypeScript version is exported as PanelWidgetProps from @leanprover/infoview.

Note that to be a good citizen which doesn't mess up the infoview layout, a panel widget should be a block element, and should provide some way to collapse it, for example by using

instance ProofWidgets.PanelWidgetProps.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.PanelWidgetProps.RpcEncodablePacket✝

Equations

• ProofWidgets.PanelWidgetProps.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.PanelWidgetProps.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.PanelWidgetProps.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.PanelWidgetProps.RpcEncodablePacket✝

Equations

• ProofWidgets.PanelWidgetProps.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.PanelWidgetProps.toJsonRpcEncodablePacket✝ }

instance ProofWidgets.PanelWidgetProps.instRpcEncodablePanelWidgetProps : Lean.Server.RpcEncodable ProofWidgets.PanelWidgetProps

Equations

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

def ProofWidgets.processIdent (stx : Lean.Syntax) (nmStx : Lean.TSyntax `ident) : Lean.CoreM Unit

Equations

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

def ProofWidgets.withPanelWidgetsTacticStx : Lean.ParserDescr

Display the selected panel widgets in the nested tactic script. For example, assuming we have written a GeometryDisplay component,

by with_panel_widgets [GeometryDisplay]
  simp
  rfl

will show the geometry display alongside the usual tactic state throughout the proof.

Equations

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

def ProofWidgets.withPanelWidgets : Lean.Elab.Tactic.Tactic

Equations

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