Documentation

Lean.Server.Completion.ImportCompletion

@[reducible, inline]
Equations
    Instances For
      @[reducible, inline]
      Equations
        Instances For
          def ImportCompletion.isImportNameCompletionRequest (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos) :

          Checks whether completionPos points at the position after an incomplete import statement.

          Equations
            Instances For
              def ImportCompletion.isImportCmdCompletionRequest (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos) :

              Checks whether completionPos points at a free space in the header.

              Equations
                Instances For
                  def ImportCompletion.computePartialImportCompletions (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos) (availableImports : ImportTrie) :
                  Equations
                    Instances For
                      def ImportCompletion.isImportCompletionRequest (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (params : Lean.Lsp.CompletionParams) :
                      Equations
                        Instances For

                          Sets the data? field of every CompletionItem in completionList using params. Ensures that completionItem/resolve requests can be routed to the correct file worker even for CompletionItems produced by the import completion.

                          Equations
                            Instances For
                              def ImportCompletion.find (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (params : Lean.Lsp.CompletionParams) (availableImports : AvailableImports) :
                              Equations
                                Instances For
                                  Equations
                                    Instances For