Documentation

Lean.Widget.InteractiveDiagnostic

source
inductive Lean.Widget.MsgEmbed:
Type
source
instance Lean.Widget.instInhabitedMsgEmbed:
Inhabited Lean.Widget.MsgEmbed
Equations
source
instance Lean.Widget.instRpcEncodingMsgEmbedRpcEncodingPacket:
(_rpcEnc : Type) → [inst : Lean.Server.RpcEncoding Lean.Widget.CodeWithInfos _rpcEnc] → (_rpcEnc_1 : Type) → [inst : Lean.Server.RpcEncoding Lean.Widget.InteractiveGoal _rpcEnc_1] → (_rpcEnc_2 : Type) → [inst : Lean.Server.RpcEncoding Nat _rpcEnc_2] → (_rpcEnc_3 : Type) → [inst : Lean.Server.RpcEncoding Lean.Name _rpcEnc_3] → (_rpcEnc_4 : Type) → [inst : Lean.Server.RpcEncoding (Lean.Server.WithRpcRef Lean.MessageData) _rpcEnc_4] → Lean.Server.RpcEncoding Lean.Widget.MsgEmbed (Lean.Widget.RpcEncodingPacket✝ _rpcEnc _rpcEnc_1 _rpcEnc_2 _rpcEnc_3 _rpcEnc_4)
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Widget.instToJsonRpcEncodingPacket_5:
{_rpcEnc _rpcEnc_1 _rpcEnc_2 _rpcEnc_3 _rpcEnc_4 : Type} → [inst : Lean.ToJson _rpcEnc] → [inst : Lean.ToJson _rpcEnc_1] → [inst : Lean.ToJson _rpcEnc_2] → [inst : Lean.ToJson _rpcEnc_3] → [inst : Lean.ToJson _rpcEnc_4] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ _rpcEnc _rpcEnc_1 _rpcEnc_2 _rpcEnc_3 _rpcEnc_4)
Equations
  • Lean.Widget.instToJsonRpcEncodingPacket_5 = { toJson := [anonymous] }
source
instance Lean.Widget.instFromJsonRpcEncodingPacket_5:
{_rpcEnc _rpcEnc_1 _rpcEnc_2 _rpcEnc_3 _rpcEnc_4 : Type} → [inst : Lean.FromJson _rpcEnc] → [inst : Lean.FromJson _rpcEnc_1] → [inst : Lean.FromJson _rpcEnc_2] → [inst : Lean.FromJson _rpcEnc_3] → [inst : Lean.FromJson _rpcEnc_4] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ _rpcEnc _rpcEnc_1 _rpcEnc_2 _rpcEnc_3 _rpcEnc_4)
Equations
  • Lean.Widget.instFromJsonRpcEncodingPacket_5 = { fromJson? := [anonymous] }
source
@[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
source
instance Lean.Widget.instFromJsonRpcEncodingPacket_6:
{range severity? code? source? message tags? relatedInformation? : Type} → [inst : Lean.FromJson range] → [inst : Lean.FromJson severity?] → [inst : Lean.FromJson code?] → [inst : Lean.FromJson source?] → [inst : Lean.FromJson message] → [inst : Lean.FromJson tags?] → [inst : Lean.FromJson relatedInformation?] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ range severity? code? source? message tags? relatedInformation?)
Equations
  • Lean.Widget.instFromJsonRpcEncodingPacket_6 = { fromJson? := [anonymous] }
source
instance Lean.Widget.instToJsonRpcEncodingPacket_6:
{range severity? code? source? message tags? relatedInformation? : Type} → [inst : Lean.ToJson range] → [inst : Lean.ToJson severity?] → [inst : Lean.ToJson code?] → [inst : Lean.ToJson source?] → [inst : Lean.ToJson message] → [inst : Lean.ToJson tags?] → [inst : Lean.ToJson relatedInformation?] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ range severity? code? source? message tags? relatedInformation?)
Equations
  • Lean.Widget.instToJsonRpcEncodingPacket_6 = { toJson := [anonymous] }
source
instance Lean.Widget.instRpcEncodingDiagnosticWithRpcEncodingPacket (α : Type) :
(range : Type) → [inst : Lean.Server.RpcEncoding Lean.Lsp.Range range] → (severity? : Type) → [inst : Lean.Server.RpcEncoding Lean.Lsp.DiagnosticSeverity severity?] → (code? : Type) → [inst : Lean.Server.RpcEncoding Lean.Lsp.DiagnosticCode code?] → (source? : Type) → [inst : Lean.Server.RpcEncoding String source?] → (message : Type) → [inst : Lean.Server.RpcEncoding α message] → (tags? : Type) → [inst : Lean.Server.RpcEncoding (Array Lean.Lsp.DiagnosticTag) tags?] → (relatedInformation? : Type) → [inst : Lean.Server.RpcEncoding (Array Lean.Lsp.DiagnosticRelatedInformation) relatedInformation?] → Lean.Server.RpcEncoding (Lean.Lsp.DiagnosticWith α) (Lean.Widget.RpcEncodingPacket✝ range severity? code? source? message tags? relatedInformation?)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
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.
source
instance Lean.Widget.instInhabitedEmbedFmt:
Inhabited Lean.Widget.EmbedFmt
Equations
source
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.
source
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.