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

inductive Lean.Widget.DiffTag : Type

• wasChanged: Lean.Widget.DiffTag
• willChange: Lean.Widget.DiffTag
• wasDeleted: Lean.Widget.DiffTag
• willDelete: Lean.Widget.DiffTag
• wasInserted: Lean.Widget.DiffTag
• willInsert: Lean.Widget.DiffTag

A tag indicating the diff status of the expression. Used when showing tactic diffs.

instance Lean.Widget.instToJsonDiffTag : Lean.ToJson Lean.Widget.DiffTag

instance Lean.Widget.instFromJsonDiffTag : Lean.FromJson Lean.Widget.DiffTag

structure Lean.Widget.SubexprInfo : Type

• info : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx

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

• subexprPos : Lean.SubExpr.Pos

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

• diffStatus? : Option Lean.Widget.DiffTag

  In certain situations such as when goal states change between positions in a tactic-mode proof, we can show subexpression-level diffs between two expressions. This field asks the renderer to display the subexpression as in a diff view (e.g. red/green like git diff).

Information about a subexpression within delaborated code.

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

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

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

@[inline, reducible]

abbrev Lean.Widget.CodeWithInfos : Type

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

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

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

def Lean.Widget.SubexprInfo.withDiffTag (tag : Lean.Widget.DiffTag) (c : Lean.Widget.SubexprInfo) : Lean.Widget.SubexprInfo

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

Tags pretty-printed code with infos from the delaborator.

partial def Lean.Widget.tagCodeInfos.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