Lean.Widget.InteractiveCode

source

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

source

instance Lean.Widget.instToJsonDiffTag :

ToJson DiffTag

Equations

source

instance Lean.Widget.instFromJsonDiffTag :

FromJson DiffTag

Equations

source

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

source

instance Lean.Widget.instRpcEncodableSubexprInfo :

Server.RpcEncodable SubexprInfo

Equations

source

@[reducible, inline]

abbrev Lean.Widget.CodeWithInfos :

Type

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

Equations

source

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

source

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

String

Equations

source

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

SubexprInfo

Equations

source

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

CodeWithInfos

Tags pretty-printed code with infos from the delaborator.

Equations

source

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

TaggedText SubexprInfo

source

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