Documentation

Lean.Server.FileWorker.SemanticHighlighting

SyntaxNodeKinds for which the syntax node and its children receive no semantic highlighting.

Equations
    Instances For

      Keywords for which a specific semantic token is provided.

      Equations
        Instances For

          Semantic token information for a given Syntax.

          Instances For

            Semantic token information with absolute LSP positions.

            Instances For

              Given a set of LeanSemanticToken, computes the AbsoluteLspSemanticToken with absolute LSP position information for each token.

              Equations
                Instances For

                  Filters all duplicate semantic tokens with the same pos, tailPos and type.

                  Equations
                    Instances For

                      Collects all semantic tokens that can be deduced purely from Syntax without elaboration information.

                      Collects all semantic tokens from the given Elab.InfoTree.

                      Equations
                        Instances For

                          Computes the semantic tokens in the range provided by p.

                          Equations
                            Instances For