max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: only consider dot completion info occurring in the hover line

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-02 09:48:03 -07:00
parent 8c2ba16f74
commit bc44ad65ae
1 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/Server/FileWorker.lean
View file

@ -366,7 +366,9 @@ section RequestHandling
open Elab in open Meta in
private partial def findCompletions? (doc : EditableDocument) (hoverPos : String.Pos) (infoTree : InfoTree) : IO (Option CompletionList) := do
if let some (ctx, Info.ofDotCompletionInfo info) := infoTree.foldInfo (init := none) choose then
let fileMap := doc.meta.text
let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
if let some (ctx, Info.ofDotCompletionInfo info) := infoTree.foldInfo (init := none) (choose fileMap hoverLine) then
info.runMetaM ctx do
let type ← instantiateMVars (← inferType info.expr)
match type.getAppFn with
@ -381,17 +383,20 @@ section RequestHandling
else
return none
where
choose (ctx : ContextInfo) (info : Info) (best? : Option (ContextInfo × Info)) : Option (ContextInfo × Info) :=
choose (fileMap : FileMap) (hoverLine : Nat) (ctx : ContextInfo) (info : Info) (best? : Option (ContextInfo × Info)) : Option (ContextInfo × Info) :=
if !info.isDotCompletion then best?
else if let some d := info.occursBefore? hoverPos then
match best? with
| none => return (ctx, info)
| some (_, best) =>
let dBest := best.occursBefore? hoverPos |>.get!
if d < dBest || (d == dBest && info.isSmaller best) then
return (ctx, info)
else
best?
let pos := info.tailPos?.get!
let ⟨line, _⟩ := fileMap.toPosition pos
if line != hoverLine then best?
else match best? with
| none => return (ctx, info)
| some (_, best) =>
let dBest := best.occursBefore? hoverPos |>.get!
if d < dBest || (d == dBest && info.isSmaller best) then
return (ctx, info)
else
best?
else
best?