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

- strict {α β : Type} : α → StrictOrLazy α β
- lazy {α β : Type} : β → StrictOrLazy α β

Instances For

source
def Lean.Widget.instInhabitedStrictOrLazy.default {a✝ : Type} [Inhabited a✝] {a✝¹ : Type} :
StrictOrLazy a✝ a✝¹
Equations

- Lean.Widget.instInhabitedStrictOrLazy.default = Lean.Widget.StrictOrLazy.strict default

Instances For

source
instance Lean.Widget.instInhabitedStrictOrLazy {a✝ : Type} [Inhabited a✝] {a✝¹ : Type} :
Inhabited (StrictOrLazy a✝ a✝¹)
Equations

- Lean.Widget.instInhabitedStrictOrLazy = { default := Lean.Widget.instInhabitedStrictOrLazy.default }

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

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

source
structure Lean.Widget.LazyTraceChildren :
Type

- indent : Nat
- children : Array (Server.WithRpcRef MessageData)

Instances For

source
instance Lean.Widget.instTypeNameLazyTraceChildren :
TypeName LazyTraceChildren
Equations

- Lean.Widget.instTypeNameLazyTraceChildren = Lean.Widget.inst✝

source
inductive Lean.Widget.MsgEmbed :
Type

- expr : CodeWithInfos → 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 : InteractiveGoal → MsgEmbed

  An interactive goal display.

- widget (wi : WidgetInstance) (alt : TaggedText MsgEmbed) : 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 (indent : Nat) (cls : Name) (msg : TaggedText MsgEmbed) (collapsed : Bool) (children : StrictOrLazy (Array (TaggedText MsgEmbed)) (Server.WithRpcRef LazyTraceChildren)) : MsgEmbed

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

Instances For

source
instance Lean.Widget.instInhabitedMsgEmbed :
Inhabited MsgEmbed
Equations

- Lean.Widget.instInhabitedMsgEmbed = { default := Lean.Widget.instInhabitedMsgEmbed.default }

source
def Lean.Widget.instInhabitedMsgEmbed.default :
MsgEmbed
Equations

- Lean.Widget.instInhabitedMsgEmbed.default = Lean.Widget.MsgEmbed.expr default

Instances For

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

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

source
@[reducible, inline]
abbrev Lean.Widget.InteractiveMessage :
Type
Equations

- Lean.Widget.InteractiveMessage = Lean.Widget.TaggedText Lean.Widget.MsgEmbed

Instances For

source
instance Lean.Widget.instTypeNameInteractiveMessage :
TypeName InteractiveMessage
Equations

- Lean.Widget.instTypeNameInteractiveMessage = Lean.Widget.instTypeNameInteractiveMessage.unsafe_impl_3

source
@[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 `.tag`s 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.InteractiveMessage

Instances For

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

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

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

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

Instances For

The `msgToInteractive` algorithm turns a `MessageData` into `InteractiveMessage` 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 `.tag`s), 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 `InteractiveMessage` 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 → InteractiveMessage` step because that would effectively require reimplementing the (stateful, to keep track of indentation) `Format.prettyM` algorithm.

source
def Lean.Widget.msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent : Nat := 0) :
IO InteractiveMessage
Equations

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

Instances For

source
def Lean.Widget.msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool) :
BaseIO 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.

Instances For