Registers all widget-related RPC procedures.

structure Lean.Widget.MsgToInteractive : Type

• msg : Lean.Server.WithRpcRef Lean.MessageData
• indent : Nat

instance Lean.Widget.instInhabitedMsgToInteractive : Inhabited Lean.Widget.MsgToInteractive

Equations

• Lean.Widget.instInhabitedMsgToInteractive = { default := { msg := default, indent := default } }

instance Lean.Widget.Lean.Widget.MsgToInteractive.instRpcEncodableMsgToInteractive : Lean.Server.RpcEncodable Lean.Widget.MsgToInteractive

Equations

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

instance Lean.Widget.Lean.Widget.MsgToInteractive.instToJsonRpcEncodablePacket : Lean.ToJson Lean.Widget.Lean.Widget.MsgToInteractive.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.MsgToInteractive.instToJsonRpcEncodablePacket = { toJson := Lean.Widget.Lean.Widget.MsgToInteractive.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.Lean.Widget.MsgToInteractive.instFromJsonRpcEncodablePacket : Lean.FromJson Lean.Widget.Lean.Widget.MsgToInteractive.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.MsgToInteractive.instFromJsonRpcEncodablePacket = { fromJson? := Lean.Widget.Lean.Widget.MsgToInteractive.fromJsonRpcEncodablePacket✝ }

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 Lean.Widget.CodeWithInfos
• exprExplicit : Option Lean.Widget.CodeWithInfos

  Show the term with the implicit arguments.

• doc : Option String

  Docstring. In markdown.

instance Lean.Widget.instInhabitedInfoPopup : Inhabited Lean.Widget.InfoPopup

Equations

• Lean.Widget.instInhabitedInfoPopup = { default := { type := default, exprExplicit := default, doc := default } }

instance Lean.Widget.Lean.Widget.InfoPopup.instToJsonRpcEncodablePacket : Lean.ToJson Lean.Widget.Lean.Widget.InfoPopup.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.InfoPopup.instToJsonRpcEncodablePacket = { toJson := Lean.Widget.Lean.Widget.InfoPopup.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.Lean.Widget.InfoPopup.instFromJsonRpcEncodablePacket : Lean.FromJson Lean.Widget.Lean.Widget.InfoPopup.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.InfoPopup.instFromJsonRpcEncodablePacket = { fromJson? := Lean.Widget.Lean.Widget.InfoPopup.fromJsonRpcEncodablePacket✝ }

instance Lean.Widget.Lean.Widget.InfoPopup.instRpcEncodableInfoPopup : Lean.Server.RpcEncodable Lean.Widget.InfoPopup

Equations

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

def Lean.Widget.makePopup : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Widget.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.

Equations

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

def Lean.Widget.makePopup.ppExprTaggedWithoutTopLevelHighlight (e : Lean.Expr) (explicit : Bool) : Lean.MetaM Lean.Widget.CodeWithInfos

Equations

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

structure Lean.Widget.GetInteractiveDiagnosticsParams : Type

• lineRange? : Option Lean.Lsp.LineRange

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

instance Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams : Inhabited Lean.Widget.GetInteractiveDiagnosticsParams

Equations

• Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams = { default := { lineRange? := default } }

instance Lean.Widget.instFromJsonGetInteractiveDiagnosticsParams : Lean.FromJson Lean.Widget.GetInteractiveDiagnosticsParams

Equations

• Lean.Widget.instFromJsonGetInteractiveDiagnosticsParams = { fromJson? := Lean.Widget.fromJsonGetInteractiveDiagnosticsParams✝ }

instance Lean.Widget.instToJsonGetInteractiveDiagnosticsParams : Lean.ToJson Lean.Widget.GetInteractiveDiagnosticsParams

Equations

• Lean.Widget.instToJsonGetInteractiveDiagnosticsParams = { toJson := Lean.Widget.toJsonGetInteractiveDiagnosticsParams✝ }

def Lean.Widget.getInteractiveDiagnostics (params : Lean.Widget.GetInteractiveDiagnosticsParams) : Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Widget.InteractiveDiagnostic))

Equations

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

structure Lean.Widget.GetGoToLocationParams : Type

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

instance Lean.Widget.Lean.Widget.GetGoToLocationParams.instRpcEncodableGetGoToLocationParams : Lean.Server.RpcEncodable Lean.Widget.GetGoToLocationParams

Equations

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

instance Lean.Widget.Lean.Widget.GetGoToLocationParams.instFromJsonRpcEncodablePacket : Lean.FromJson Lean.Widget.Lean.Widget.GetGoToLocationParams.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.GetGoToLocationParams.instFromJsonRpcEncodablePacket = { fromJson? := Lean.Widget.Lean.Widget.GetGoToLocationParams.fromJsonRpcEncodablePacket✝ }

instance Lean.Widget.Lean.Widget.GetGoToLocationParams.instToJsonRpcEncodablePacket : Lean.ToJson Lean.Widget.Lean.Widget.GetGoToLocationParams.RpcEncodablePacket✝

Equations

• Lean.Widget.Lean.Widget.GetGoToLocationParams.instToJsonRpcEncodablePacket = { toJson := Lean.Widget.Lean.Widget.GetGoToLocationParams.toJsonRpcEncodablePacket✝ }

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

Equations

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