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} [Lean.Server.RpcEncodable α] [Lean.Server.RpcEncodable β] : Lean.Server.RpcEncodable (Lean.Widget.StrictOrLazy α β)

Equations

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

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

  A piece of Lean code with elaboration/typing data. Note: does not necessarily correspond to an Expr, the name is for RPC API compatibility.

• goal: Lean.Widget.InteractiveGoal → Lean.Widget.MsgEmbed

  An interactive goal display.

• widget: Lean.Widget.WidgetInstance → Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Lean.Widget.MsgEmbed

  A widget instance.

  alt is a fallback rendering of the widget that can be shown in standard, non-interactive LSP diagnostics, as well as when user widgets are not supported by the client.

• trace: Nat → Lake.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

  Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow the user to expand sub-traces interactively.

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lean.Widget.InteractiveDiagnostic : Type

The message field is the text of a message possibly containing interactive embeds of type MsgEmbed. We maintain the invariant that embeds are stored in .tags with empty .text subtrees, i.e., .tag embed (.text "").

Client-side display algorithms render tags in a custom way, ignoring the nested text.

Equations

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

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

Equations

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

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.

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

def Lean.Widget.InteractiveDiagnostic.compareAsDiagnostics (a : Lean.Widget.InteractiveDiagnostic) (b : Lean.Widget.InteractiveDiagnostic) : Ordering

Compares interactive diagnostics modulo TaggedText tags and traces.

Equations

• a.compareAsDiagnostics b = Lean.Lsp.compareByUserVisible a.toDiagnostic b.toDiagnostic

The msgToInteractive algorithm turns a MessageData into TaggedText MsgEmbed in two stages.

First, in msgToInteractiveAux we produce a Format object whose .tag nodes refer to EmbedFmt objects stored in an auxiliary array. Only the most shallow .tag in every branch through the Format corresponds to an EmbedFmt. The kind of this tag determines how the nested Format object (possibly including further .tags), is processed. For example, if the output is .tag (.expr ctx infos) fmt then tags in the nested fmt object refer to elements of infos.

In the second stage, we recursively transform such a Format into TaggedText MsgEmbed according to the rule above by first pretty-printing it and then grabbing data referenced by the tags from all the nested arrays (such as the infos array in the example above).

We cannot easily do the translation in a single MessageData → TaggedText MsgEmbed step because that would effectively require reimplementing the (stateful, to keep track of indentation) Format.prettyM algorithm.

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

Equations

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

opaque Lean.Widget.infoview.maxTraceChildren : Lean.Option Nat

Number of trace node children to display by default in the info view in order to prevent slowdowns from rendering.

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) : BaseIO 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.