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

inductive Lean.Widget.DiffTag : Type

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

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

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

Equations

• Lean.Widget.instToJsonDiffTag = { toJson := Lean.Widget.toJsonDiffTag✝ }

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

Equations

• Lean.Widget.instFromJsonDiffTag = { fromJson? := Lean.Widget.fromJsonDiffTag✝ }

structure Lean.Widget.SubexprInfo : Type

Information about a subexpression within delaborated code.

• 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).

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

Equations

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

@[reducible, 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} [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

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

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

Equations

• Lean.Widget.SubexprInfo.withDiffTag tag c = { info := c.info, subexprPos := c.subexprPos, diffStatus? := some tag }

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.

Equations

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

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

Equations

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