Registers all widget-related RPC procedures.

structure Lean.Widget.MsgToInteractive : Type

• msg : Server.WithRpcRef MessageData
• indent : Nat

instance Lean.Widget.instInhabitedMsgToInteractive : Inhabited MsgToInteractive

Equations

• Lean.Widget.instInhabitedMsgToInteractive = { default := Lean.Widget.instInhabitedMsgToInteractive.default }

def Lean.Widget.instInhabitedMsgToInteractive.default : MsgToInteractive

Equations

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

instance Lean.Widget.instRpcEncodableMsgToInteractive : Server.RpcEncodable MsgToInteractive

Equations

• Lean.Widget.instRpcEncodableMsgToInteractive = { rpcEncode := Lean.Widget.instRpcEncodableMsgToInteractive.enc✝, rpcDecode := Lean.Widget.instRpcEncodableMsgToInteractive.dec✝ }

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

Equations

• Lean.Widget.instInhabitedInfoPopup = { default := Lean.Widget.instInhabitedInfoPopup.default }

def Lean.Widget.instInhabitedInfoPopup.default : InfoPopup

Equations

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

instance Lean.Widget.instRpcEncodableInfoPopup : Server.RpcEncodable InfoPopup

Equations

• Lean.Widget.instRpcEncodableInfoPopup = { rpcEncode := Lean.Widget.instRpcEncodableInfoPopup.enc✝, rpcDecode := Lean.Widget.instRpcEncodableInfoPopup.dec✝ }

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.

Equations

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

structure Lean.Widget.GetInteractiveDiagnosticsParams : Type

• lineRange? : Option Lsp.LineRange

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

def Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams.default : GetInteractiveDiagnosticsParams

Equations

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

instance Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams : Inhabited GetInteractiveDiagnosticsParams

Equations

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

def Lean.Widget.instFromJsonGetInteractiveDiagnosticsParams.fromJson : Json → Except String GetInteractiveDiagnosticsParams

Equations

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

instance Lean.Widget.instFromJsonGetInteractiveDiagnosticsParams : FromJson GetInteractiveDiagnosticsParams

Equations

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

def Lean.Widget.instToJsonGetInteractiveDiagnosticsParams.toJson : GetInteractiveDiagnosticsParams → Json

Equations

• Lean.Widget.instToJsonGetInteractiveDiagnosticsParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "lineRange" x✝.lineRange?].flatten

instance Lean.Widget.instToJsonGetInteractiveDiagnosticsParams : ToJson GetInteractiveDiagnosticsParams

Equations

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

structure Lean.Widget.GetGoToLocationParams : Type

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

instance Lean.Widget.instRpcEncodableGetGoToLocationParams : Server.RpcEncodable GetGoToLocationParams

Equations

• Lean.Widget.instRpcEncodableGetGoToLocationParams = { rpcEncode := Lean.Widget.instRpcEncodableGetGoToLocationParams.enc✝, rpcDecode := Lean.Widget.instRpcEncodableGetGoToLocationParams.dec✝ }

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

Equations

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

inductive Lean.Widget.HighlightedSubexprInfo : Type

• subexpr (info : SubexprInfo) : HighlightedSubexprInfo
• highlighted : HighlightedSubexprInfo

instance Lean.Widget.instRpcEncodableHighlightedSubexprInfo : Server.RpcEncodable HighlightedSubexprInfo

Equations

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

@[reducible, inline]

abbrev Lean.Widget.HighlightedCodeWithInfos : Type

Equations

• Lean.Widget.HighlightedCodeWithInfos = Lean.Widget.TaggedText Lean.Widget.HighlightedSubexprInfo

inductive Lean.Widget.HighlightedMsgEmbed : Type

• expr : HighlightedCodeWithInfos → HighlightedMsgEmbed
• goal : InteractiveGoal → HighlightedMsgEmbed
• widget (wi : WidgetInstance) (alt : TaggedText HighlightedMsgEmbed) : HighlightedMsgEmbed
• trace (indent : Nat) (cls : Name) (msg : TaggedText HighlightedMsgEmbed) (collapsed : Bool) (children : StrictOrLazy (Array (TaggedText HighlightedMsgEmbed)) (Server.WithRpcRef LazyTraceChildren)) : HighlightedMsgEmbed
• highlighted : HighlightedMsgEmbed

def Lean.Widget.instInhabitedHighlightedMsgEmbed.default : HighlightedMsgEmbed

Equations

• Lean.Widget.instInhabitedHighlightedMsgEmbed.default = Lean.Widget.HighlightedMsgEmbed.expr default

instance Lean.Widget.instInhabitedHighlightedMsgEmbed : Inhabited HighlightedMsgEmbed

Equations

• Lean.Widget.instInhabitedHighlightedMsgEmbed = { default := Lean.Widget.instInhabitedHighlightedMsgEmbed.default }

instance Lean.Widget.instRpcEncodableHighlightedMsgEmbed : Server.RpcEncodable HighlightedMsgEmbed

Equations

• Lean.Widget.instRpcEncodableHighlightedMsgEmbed = { rpcEncode := Lean.Widget.instRpcEncodableHighlightedMsgEmbed.enc✝, rpcDecode := Lean.Widget.instRpcEncodableHighlightedMsgEmbed.dec✝ }

@[reducible, inline]

abbrev Lean.Widget.HighlightedInteractiveMessage : Type

Equations

• Lean.Widget.HighlightedInteractiveMessage = Lean.Widget.TaggedText Lean.Widget.HighlightedMsgEmbed

structure Lean.Widget.HighlightMatchesParams : Type

• query : String
• msg : InteractiveMessage

instance Lean.Widget.instRpcEncodableHighlightMatchesParams : Server.RpcEncodable HighlightMatchesParams

Equations

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

def Lean.Widget.highlightMatches (params : HighlightMatchesParams) : Server.RequestM (Server.RequestTask HighlightedInteractiveMessage)

Equations

• Lean.Widget.highlightMatches params = (do let r ← liftM (Lean.Widget.highlightMatchesAux✝ params.query params.msg) pure (Lean.Widget.Highlighted.msg✝ r)).pureTask