Documentation

Lean.Server.InfoUtils

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 ctx and info.lctx).

W.r.t. widgets, this is used to tag different parts of expressions in ppExprTagged. This is the input to the RPC call Lean.Widget.InteractiveDiagnostics.infoToInteractive. 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 Lean.Server.FileWorker.locationLinksOfInfo), all the elaborator information we need for similar tasks is already fully recoverable via the InfoTree structure (see Lean.Elab.InfoTree.visitM). 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.

Instances For

    Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up.

    Equations
    Instances For

      InfoTree.visitM specialized to Unit return type

      Equations
      Instances For

        Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves).

        Equations
        Instances For

          For every branch of the InfoTree, find the deepest node in that branch for which p returns some _ and return the union of all such nodes. The visitor p is given a node together with its innermost surrounding ContextInfo.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.Elab.InfoTree.foldInfo {α : Type u_1} (f : Lean.Elab.ContextInfoLean.Elab.Infoαα) (init : α) :
            Equations
            Instances For
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Find an info node, if any, which should be shown on hover/cursor at position hoverPos.

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

                                        Construct a hover popup, if any, from an info node in a context.

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

                                                Try to retrieve TacticInfo for hoverPos. 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. However, if hoverPos is after the tactic, we prefer nodes that are not indented relative to it, meaning that e.g. at | in

                                                have := by
                                                  exact foo
                                                |
                                                

                                                we show the (final, see below) state of have, not exact.

                                                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 withTacticInfoContext)
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For