Registers all widget-related RPC procedures.

structure Lean.Widget.MsgToInteractive : Type

• msg : Server.WithRpcRef MessageData
• indent : Nat

instance Lean.Widget.instInhabitedMsgToInteractive : Inhabited MsgToInteractive

instance Lean.Widget.instRpcEncodableMsgToInteractive : Server.RpcEncodable MsgToInteractive

structure Lean.Widget.InfoPopup : Type

The information that the infoview uses to render a popup for when the user hovers over an expression.

• type : Option CodeWithInfos
• exprExplicit : Option CodeWithInfos

  Show the term with the implicit arguments.

• doc : Option String

  Docstring. In markdown.

instance Lean.Widget.instInhabitedInfoPopup : Inhabited InfoPopup

instance Lean.Widget.instRpcEncodableInfoPopup : Server.RpcEncodable InfoPopup

def Lean.Widget.makePopup : Server.WithRpcRef Elab.InfoWithCtx → Server.RequestM (Server.RequestTask InfoPopup)

Given elaborator info for a particular subexpression. Produce the InfoPopup.

The intended usage of this is for the infoview to pass the InfoWithCtx which was stored for a particular SubexprInfo tag in a TaggedText generated with ppExprTagged.

def Lean.Widget.makePopup.maybeWithoutTopLevelHighlight : Bool → CodeWithInfos → CodeWithInfos

def Lean.Widget.makePopup.ppExprForPopup (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos

structure Lean.Widget.GetInteractiveDiagnosticsParams : Type

• lineRange? : Option Lsp.LineRange

  Return diagnostics for these lines only if present, otherwise return all diagnostics.

instance Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams : Inhabited GetInteractiveDiagnosticsParams

instance Lean.Widget.instFromJsonGetInteractiveDiagnosticsParams : FromJson GetInteractiveDiagnosticsParams

instance Lean.Widget.instToJsonGetInteractiveDiagnosticsParams : ToJson GetInteractiveDiagnosticsParams

structure Lean.Widget.GetGoToLocationParams : Type

• kind : Server.GoToKind
• info : Server.WithRpcRef Elab.InfoWithCtx

instance Lean.Widget.instRpcEncodableGetGoToLocationParams : Server.RpcEncodable GetGoToLocationParams

def Lean.Widget.lazyTraceChildrenToInteractive (children : Server.WithRpcRef LazyTraceChildren) : Server.RequestM (Server.RequestTask (Array (TaggedText MsgEmbed)))