Documentation

Lean.Server.FileWorker.WidgetRequests

Registers all widget-related RPC procedures.

source
structure Lean.Widget.MsgToInteractive:
Type
source
instance Lean.Widget.instInhabitedMsgToInteractive:
Inhabited Lean.Widget.MsgToInteractive
Equations
source
instance Lean.Widget.instRpcEncodingMsgToInteractiveRpcEncodingPacket:
(msg : Type) → [inst : Lean.Server.RpcEncoding (Lean.Server.WithRpcRef Lean.MessageData) msg] → (indent : Type) → [inst : Lean.Server.RpcEncoding Nat indent] → Lean.Server.RpcEncoding Lean.Widget.MsgToInteractive (Lean.Widget.RpcEncodingPacket✝ msg indent)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Widget.instToJsonRpcEncodingPacket_7:
{msg indent : Type} → [inst : Lean.ToJson msg] → [inst : Lean.ToJson indent] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ msg indent)
Equations
  • Lean.Widget.instToJsonRpcEncodingPacket_7 = { toJson := [anonymous] }
source
instance Lean.Widget.instFromJsonRpcEncodingPacket_7:
{msg indent : Type} → [inst : Lean.FromJson msg] → [inst : Lean.FromJson indent] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ msg indent)
Equations
  • Lean.Widget.instFromJsonRpcEncodingPacket_7 = { fromJson? := [anonymous] }
source
structure Lean.Widget.InfoPopup:
Type

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

source
instance Lean.Widget.instInhabitedInfoPopup:
Inhabited Lean.Widget.InfoPopup
Equations
source
instance Lean.Widget.instRpcEncodingInfoPopupRpcEncodingPacket:
(type : Type) → [inst : Lean.Server.RpcEncoding (Option Lean.Widget.CodeWithInfos) type] → (doc : Type) → [inst : Lean.Server.RpcEncoding (Option String) doc] → Lean.Server.RpcEncoding Lean.Widget.InfoPopup (Lean.Widget.RpcEncodingPacket✝ type doc)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Widget.instFromJsonRpcEncodingPacket_8:
{type doc : Type} → [inst : Lean.FromJson type] → [inst : Lean.FromJson doc] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ type doc)
Equations
  • Lean.Widget.instFromJsonRpcEncodingPacket_8 = { fromJson? := [anonymous] }
source
instance Lean.Widget.instToJsonRpcEncodingPacket_8:
{type doc : Type} → [inst : Lean.ToJson type] → [inst : Lean.ToJson doc] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ type doc)
Equations
  • Lean.Widget.instToJsonRpcEncodingPacket_8 = { toJson := [anonymous] }
source
def Lean.Widget.makePopup:
Lean.Server.WithRpcRef Lean.Widget.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.
source
structure Lean.Widget.GetInteractiveDiagnosticsParams:
Type

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

    lineRange? : Option Lean.Lsp.LineRange
source
instance Lean.Widget.instInhabitedGetInteractiveDiagnosticsParams:
Inhabited Lean.Widget.GetInteractiveDiagnosticsParams
Equations
source
instance Lean.Widget.instFromJsonGetInteractiveDiagnosticsParams:
Lean.FromJson Lean.Widget.GetInteractiveDiagnosticsParams
Equations
source
instance Lean.Widget.instToJsonGetInteractiveDiagnosticsParams:
Lean.ToJson Lean.Widget.GetInteractiveDiagnosticsParams
Equations
source
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.
source
structure Lean.Widget.GetGoToLocationParams:
Type
source
instance Lean.Widget.instToJsonRpcEncodingPacket_9:
{kind info : Type} → [inst : Lean.ToJson kind] → [inst : Lean.ToJson info] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ kind info)
Equations
  • Lean.Widget.instToJsonRpcEncodingPacket_9 = { toJson := [anonymous] }
source
instance Lean.Widget.instRpcEncodingGetGoToLocationParamsRpcEncodingPacket:
(kind : Type) → [inst : Lean.Server.RpcEncoding Lean.Server.GoToKind kind] → (info : Type) → [inst : Lean.Server.RpcEncoding (Lean.Server.WithRpcRef Lean.Widget.InfoWithCtx) info] → Lean.Server.RpcEncoding Lean.Widget.GetGoToLocationParams (Lean.Widget.RpcEncodingPacket✝ kind info)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Widget.instFromJsonRpcEncodingPacket_9:
{kind info : Type} → [inst : Lean.FromJson kind] → [inst : Lean.FromJson info] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ kind info)
Equations
  • Lean.Widget.instFromJsonRpcEncodingPacket_9 = { fromJson? := [anonymous] }