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 : DiffTag
• willChange : DiffTag
• wasDeleted : DiffTag
• willDelete : DiffTag
• wasInserted : DiffTag
• willInsert : DiffTag

def Lean.Widget.instToJsonDiffTag.toJson : DiffTag → Json

Equations

• Lean.Widget.instToJsonDiffTag.toJson Lean.Widget.DiffTag.wasChanged = Lean.toJson "wasChanged"
• Lean.Widget.instToJsonDiffTag.toJson Lean.Widget.DiffTag.willChange = Lean.toJson "willChange"
• Lean.Widget.instToJsonDiffTag.toJson Lean.Widget.DiffTag.wasDeleted = Lean.toJson "wasDeleted"
• Lean.Widget.instToJsonDiffTag.toJson Lean.Widget.DiffTag.willDelete = Lean.toJson "willDelete"
• Lean.Widget.instToJsonDiffTag.toJson Lean.Widget.DiffTag.wasInserted = Lean.toJson "wasInserted"
• Lean.Widget.instToJsonDiffTag.toJson Lean.Widget.DiffTag.willInsert = Lean.toJson "willInsert"

instance Lean.Widget.instToJsonDiffTag : ToJson DiffTag

Equations

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

def Lean.Widget.instFromJsonDiffTag.fromJson : Json → Except String DiffTag

Equations

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

instance Lean.Widget.instFromJsonDiffTag : FromJson DiffTag

Equations

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

structure Lean.Widget.SubexprInfo : Type

Information about a subexpression within delaborated code.

• info : Server.WithRpcRef Elab.InfoWithCtx

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

• subexprPos : SubExpr.Pos

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

• diffStatus? : Option 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 : Server.RpcEncodable 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 : SubexprInfo → α → m SubexprInfo) (pm : SubExpr.PosMap α) (tt : CodeWithInfos) : m CodeWithInfos

Equations

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

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

Equations

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

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

Equations

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

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

Tags pretty-printed code with infos from the delaborator.

Equations

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

def Lean.Widget.ppExprTagged (e : Expr) (delab : PrettyPrinter.Delaborator.Delab := PrettyPrinter.Delaborator.delab) : MetaM CodeWithInfos

Pretty prints the expression e using delaborator delab, returning an object that represents the pretty printed syntax paired with information needed to support hovers.

Equations

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