@[reducible, inline]

abbrev ImportCompletion.ImportTrie : Type

@[reducible, inline]

abbrev ImportCompletion.AvailableImports : Type

def ImportCompletion.AvailableImports.toImportTrie (imports : AvailableImports) : ImportTrie

def ImportCompletion.isImportNameCompletionRequest (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) : Bool

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.

def ImportCompletion.computePartialImportCompletions (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (completionPos : String.Pos.Raw) (availableImports : ImportTrie) : Array Lean.Name

def ImportCompletion.isImportCompletionRequest (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (params : Lean.Lsp.CompletionParams) : Bool

def ImportCompletion.collectAvailableImportsFromLake : IO (Option AvailableImports)

def ImportCompletion.collectAvailableImportsFromSrcSearchPath : IO AvailableImports

def ImportCompletion.collectAvailableImports : IO AvailableImports

def ImportCompletion.addCompletionItemData (mod : Lean.Name) (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.

def ImportCompletion.find (mod : Lean.Name) (pos : Lean.Lsp.Position) (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) (availableImports : AvailableImports) : Lean.Lsp.CompletionList

def ImportCompletion.computeCompletions (mod : Lean.Name) (pos : Lean.Lsp.Position) (text : Lean.FileMap) (headerStx : Lean.TSyntax `Lean.Parser.Module.header) : IO Lean.Lsp.CompletionList