Elaborator information with elaborator context.
It can be thought of as a "thunked" elaboration computation that allows us
to retroactively extract type information, symbol locations, etc.
through arbitrary invocations of
runMetaM (where the necessary context and state
can be reconstructed from
W.r.t. widgets, this is used to tag different parts of expressions in
This is the input to the RPC call
It carries over information about delaborated
Info nodes in a
CodeWithInfos, and the associated pretty-printing
functionality is purpose-specific to showing the contents of infoview popups.
For use in standard LSP go-to-definition (see
all the elaborator information we need for similar tasks is already fully recoverable via
InfoTree structure (see
There we use this as a convienience wrapper for queried nodes (e.g. the return value of
Lean.Elab.InfoTree.hoverableInfoAt?). It also includes the children info nodes
as additional context (this is unused in the RPC case, as delaboration has no notion of child nodes).
NOTE: This type is for internal use in the infoview/LSP. It should not be used in user widgets.
Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up.
Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves).
For every branch of the
InfoTree, find the deepest node in that branch for which
some _ and return the union of all such nodes. The visitor
p is given a node together with
its innermost surrounding
Find an info node, if any, which should be shown on hover/cursor at position
- Lean.Elab.Info.fmtHover?.isAtomicFormat (Std.Format.text a) = true
- Lean.Elab.Info.fmtHover?.isAtomicFormat (Lean.Format.group f behavior) = Lean.Elab.Info.fmtHover?.isAtomicFormat f
- Lean.Elab.Info.fmtHover?.isAtomicFormat (Lean.Format.nest indent f) = Lean.Elab.Info.fmtHover?.isAtomicFormat f
- Lean.Elab.Info.fmtHover?.isAtomicFormat (Lean.Format.tag a f) = Lean.Elab.Info.fmtHover?.isAtomicFormat f
- Lean.Elab.Info.fmtHover?.isAtomicFormat x = false
Try to retrieve
We retrieve all
TacticInfo nodes s.t.
hoverPos is inside the node's range plus trailing whitespace.
We usually prefer the innermost such nodes so that for composite tactics such as
induction, we show the nested proofs' states.
hoverPos is after the tactic, we prefer nodes that are not indented relative to it, meaning that e.g. at
have := by exact foo |
we show the (final, see below) state of
Moreover, we instruct the LSP server to use the state after tactic execution if
- the hover position is after the info's start position and
- there is no nested tactic info after the hover position (tactic combinators should decide for themselves
where to show intermediate states by calling