RPC infrastructure for storing and formatting code fragments, in particular Exprs, with environment and subexpression information.

inductive Lean.Widget.HighlightColor : Type

• green: Lean.Widget.HighlightColor
• blue: Lean.Widget.HighlightColor
• red: Lean.Widget.HighlightColor
• yellow: Lean.Widget.HighlightColor
• purple: Lean.Widget.HighlightColor

instance Lean.Widget.instToJsonHighlightColor : Lean.ToJson Lean.Widget.HighlightColor

Equations

• Lean.Widget.instToJsonHighlightColor = { toJson := Lean.Widget.toJsonHighlightColor✝ }

instance Lean.Widget.instFromJsonHighlightColor : Lean.FromJson Lean.Widget.HighlightColor

Equations

• Lean.Widget.instFromJsonHighlightColor = { fromJson? := Lean.Widget.fromJsonHighlightColor✝ }

structure Lean.Widget.SubexprInfo : Type

• The Elab.Info node with the semantics of this part of the output.

  info : Lean.Server.WithRpcRef Lean.Widget.InfoWithCtx

• The position of this subexpression within the top-level expression. See Lean.SubExpr.

  subexprPos : Lean.SubExpr.Pos

• Ask the renderer to highlight this node in the given color.

  highlightColor? : Option Lean.Widget.HighlightColor

Information about a subexpression within delaborated code.

instance Lean.Widget.instInhabitedSubexprInfo : Inhabited Lean.Widget.SubexprInfo

Equations

• Lean.Widget.instInhabitedSubexprInfo = { default := { info := default, subexprPos := default, highlightColor? := default } }

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

Equations

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

instance Lean.Widget.instRpcEncodableSubexprInfo : Lean.Server.RpcEncodable Lean.Widget.SubexprInfo

Equations

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

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

Equations

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

@[inline]

abbrev Lean.Widget.CodeWithInfos : Type

Pretty-printed syntax (usually but not necessarily an Expr) with embedded Infos.

Equations

• Lean.Widget.CodeWithInfos = Lean.Widget.TaggedText Lean.Widget.SubexprInfo

def Lean.Widget.CodeWithInfos.mergePosMap {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] (merger : Lean.Widget.SubexprInfo → α → m Lean.Widget.SubexprInfo) (pm : Lean.SubExpr.PosMap α) (tt : Lean.Widget.CodeWithInfos) : m Lean.Widget.CodeWithInfos

Equations

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

def Lean.Widget.CodeWithInfos.pretty (tt : Lean.Widget.CodeWithInfos) : String

Equations

• Lean.Widget.CodeWithInfos.pretty tt = Lean.Widget.TaggedText.stripTags tt

def Lean.Widget.SubexprInfo.highlight (color : Lean.Widget.HighlightColor) (c : Lean.Widget.SubexprInfo) : Lean.Widget.SubexprInfo

Equations

• Lean.Widget.SubexprInfo.highlight color c = { info := c.info, subexprPos := c.subexprPos, highlightColor? := some color }

def Lean.Widget.tagExprInfos (ctx : Lean.Elab.ContextInfo) (infos : Lean.SubExpr.PosMap Lean.Elab.Info) (tt : Lean.Widget.TaggedText (Nat × Nat)) : Lean.Widget.CodeWithInfos

Tags a pretty-printed Expr with infos from the delaborator.

Equations

• Lean.Widget.tagExprInfos ctx infos tt = Lean.Widget.tagExprInfos.go ctx infos tt

partial def Lean.Widget.tagExprInfos.go (ctx : Lean.Elab.ContextInfo) (infos : Lean.SubExpr.PosMap Lean.Elab.Info) (tt : Lean.Widget.TaggedText (Nat × Nat)) : Lean.Widget.TaggedText Lean.Widget.SubexprInfo

def Lean.Widget.ppExprTagged (e : Lean.Expr) (explicit : optParam Bool false) : Lean.MetaM Lean.Widget.CodeWithInfos

Equations

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