Collapsible MessageData widget

collapsible summary body produces a MessageData that renders in the infoview as a dropdown <details> element:

▼ summary
  body

summary is the header, and body is shown only when expanded. Both summary and body are MessageData.

Unlike MessageData.trace, this carries no trace styling or cls tag, and unfortunately is not lazy.

Future work

• Make the body lazy (i.e. only constructed when the dropdown is expanded).

structure ImportGraph.Widget.CollapsibleProps : Type

Props for the Collapsible widget.

• summary : Lean.Server.WithRpcRef Lean.MessageData

  The header MessageData.

• body : Lean.Server.WithRpcRef Lean.MessageData

  The hideable body revealed when the dropdown is expanded.

• initiallyOpen : Bool

  Whether the dropdown starts expanded.

@[instance_reducible]

instance ImportGraph.Widget.instRpcEncodableCollapsibleProps : Lean.Server.RpcEncodable CollapsibleProps

Equations

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

def ImportGraph.Widget.Collapsible : Lean.Widget.Module

The dropdown widget: a <details> component with MessageData header and body.

Note: The body is mounted lazily. Since an ordinary closed <details> component would still mount the body even if it were closed, we track whether the <details> component has ever been opened manually and mount it on first open. It then stays mounted.

Equations

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

def ImportGraph.Widget.collapsible {m : Type → Type} [Monad m] [MonadLiftT Lean.CoreM m] [Lean.AddMessageContext m] (summary body : Lean.MessageData) (initiallyOpen : Bool := false) : m Lean.MessageData

Build a MessageData that renders as a collapsible dropdown: summary is the header and body is the MessageData revealed when expanded. For example:

⯈ This is the header!

may be clicked to expand to

▼ This is the header!
  And this is the body.

initiallyOpen controls whether the dropdown starts expanded (default false).

Note that the body is already indented, and e.g. indentD body may insert an unwanted extra line.

Equations

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