Documentation

Lean.Server.Completion.ImportCompletion

source
@[reducible, inline]
abbrev ImportCompletion.ImportTrie :
Type
Instances For
    source
    @[reducible, inline]
    abbrev ImportCompletion.AvailableImports :
    Type
    Instances For
      source
      def ImportCompletion.AvailableImports.toImportTrie (imports : AvailableImports) :
      ImportTrie
      Instances For
        source
        def ImportCompletion.isImportNameCompletionRequest (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) :
        Bool
        Instances For
          source
          def ImportCompletion.isImportCmdCompletionRequest (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) :
          Bool

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

          Instances For
            source
            def ImportCompletion.computePartialImportCompletions (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) (availableImports : ImportTrie) :
            Array Lean.Name
            Instances For
              source
              def ImportCompletion.isImportCompletionRequest (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (params : Lean.Lsp.CompletionParams) :
              Bool
              Instances For
                source
                def ImportCompletion.collectAvailableImportsFromLake :
                IO (Option AvailableImports)
                Instances For
                  source
                  def ImportCompletion.collectAvailableImportsFromSrcSearchPath :
                  IO AvailableImports
                  Instances For
                    source
                    def ImportCompletion.collectAvailableImports :
                    IO AvailableImports
                    Instances For
                      source
                      def ImportCompletion.addCompletionItemData (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (completionList : Lean.Lsp.CompletionList) :
                      Lean.Lsp.CompletionList

                      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.

                      Instances For
                        source
                        def ImportCompletion.find (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (availableImports : AvailableImports) :
                        Lean.Lsp.CompletionList
                        Instances For
                          source
                          def ImportCompletion.computeCompletions (uri : Lean.Lsp.DocumentUri) (pos : Lean.Lsp.Position) (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) :
                          IO Lean.Lsp.CompletionList
                          Instances For