inductive Lean.Widget.StrictOrLazy (α : Type) (β : Type) : Type

• strict: {α β : Type} → α → Lean.Widget.StrictOrLazy α β
• lazy: {α β : Type} → β → Lean.Widget.StrictOrLazy α β

instance Lean.Widget.instInhabitedStrictOrLazy : {a : Type} → [inst : Inhabited a] → {a_1 : Type} → Inhabited (Lean.Widget.StrictOrLazy a a_1)

Equations

• Lean.Widget.instInhabitedStrictOrLazy = { default := Lean.Widget.StrictOrLazy.strict default }

instance Lean.Widget.instRpcEncodableStrictOrLazy {α : Type} {β : Type} [inst : Lean.Server.RpcEncodable α] [inst : Lean.Server.RpcEncodable β] : Lean.Server.RpcEncodable (Lean.Widget.StrictOrLazy α β)

Equations

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

instance Lean.Widget.instToJsonRpcEncodablePacket_5 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_5 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instFromJsonRpcEncodablePacket_5 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

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

structure Lean.Widget.LazyTraceChildren : Type

• indent : Nat
• children : Array (Lean.Server.WithRpcRef Lean.MessageData)

instance Lean.Widget.instTypeNameLazyTraceChildren : TypeName Lean.Widget.LazyTraceChildren

Equations

• Lean.Widget.instTypeNameLazyTraceChildren = Lean.Widget.inst✝

inductive Lean.Widget.MsgEmbed : Type

• expr: Lean.Widget.CodeWithInfos → Lean.Widget.MsgEmbed
• goal: Lean.Widget.InteractiveGoal → Lean.Widget.MsgEmbed
• trace: Nat → Lean.Name → Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Bool → Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) → Lean.Widget.MsgEmbed

instance Lean.Widget.instInhabitedMsgEmbed : Inhabited Lean.Widget.MsgEmbed

Equations

• Lean.Widget.instInhabitedMsgEmbed = { default := Lean.Widget.MsgEmbed.expr default }

instance Lean.Widget.instFromJsonRpcEncodablePacket_6 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

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

instance Lean.Widget.instToJsonRpcEncodablePacket_6 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_6 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instRpcEncodableMsgEmbed : Lean.Server.RpcEncodable Lean.Widget.MsgEmbed

Equations

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

@[inline]

abbrev Lean.Widget.InteractiveDiagnostic : Type

We embed objects in LSP diagnostics by storing them in the tag of an empty subtree (text ""). In other words, we terminate the MsgEmbed-tagged tree at embedded objects and instead store the pretty-printed embed (which can itself be a TaggedText) in the tag.

Equations

• Lean.Widget.InteractiveDiagnostic = Lean.Lsp.DiagnosticWith (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)

instance Lean.Widget.instRpcEncodableDiagnosticWith {α : Type} [inst : Lean.Server.RpcEncodable α] : Lean.Server.RpcEncodable (Lean.Lsp.DiagnosticWith α)

Equations

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

instance Lean.Widget.instToJsonRpcEncodablePacket_7 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_7 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instFromJsonRpcEncodablePacket_7 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

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

def Lean.Widget.InteractiveDiagnostic.toDiagnostic (diag : Lean.Widget.InteractiveDiagnostic) : Lean.Lsp.Diagnostic

Equations

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

def Lean.Widget.InteractiveDiagnostic.toDiagnostic.prettyTt (tt : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) : String

Equations

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

instance Lean.Widget.instInhabitedEmbedFmt : Inhabited Lean.Widget.EmbedFmt

Equations

• Lean.Widget.instInhabitedEmbedFmt = { default := Lean.Widget.EmbedFmt.expr default default }

def Lean.Widget.msgToInteractive (msgData : Lean.MessageData) (hasWidgets : Bool) (indent : optParam Nat 0) : IO (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)

Equations

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

partial def Lean.Widget.msgToInteractive.fmtToTT (embeds : Array Lean.Widget.EmbedFmt) (fmt : Lean.Format) (indent : Nat) : IO (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)

def Lean.Widget.msgToInteractiveDiagnostic (text : Lean.FileMap) (m : Lean.Message) (hasWidgets : Bool) : IO Lean.Widget.InteractiveDiagnostic

Transform a Lean Message concerning the given text into an LSP Diagnostic.

Equations

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