diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 4c8d36290b7d..cb36ed7a0785 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -182,7 +182,9 @@ end Utils section IdCompletionUtils - private def matchAtomic (id : Name) (declName : Name) : Option Float := + private def matchAtomic (id : Name) (declName : Name) (danglingDot : Bool) : Option Float := do + if danglingDot then + none match id, declName with | .str .anonymous s₁, .str .anonymous s₂ => fuzzyMatchScoreWithThreshold? s₁ s₂ | _, _ => none @@ -360,7 +362,7 @@ private def idCompletionCore if id.isAtomic then -- search for matches in the local context for localDecl in (← getLCtx) do - if let some score := matchAtomic id localDecl.userName then + if let some score := matchAtomic id localDecl.userName danglingDot then addUnresolvedCompletionItem localDecl.userName (.fvar localDecl.fvarId) (kind := CompletionItemKind.variable) score -- search for matches in the environment let env ← getEnv @@ -395,10 +397,11 @@ private def idCompletionCore matchUsingNamespace Name.anonymous if let some (bestLabel, bestScore) := bestMatch? then addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) bestScore - -- Recall that aliases may not be atomic and include the namespace where they were created. let matchAlias (ns : Name) (alias : Name) : Option Float := + -- Recall that aliases may not be atomic and include the namespace where they were created. if ns.isPrefixOf alias then - matchAtomic id (alias.replacePrefix ns Name.anonymous) + let alias := alias.replacePrefix ns Name.anonymous + matchAtomic id alias danglingDot else none let eligibleHeaderDecls ← getEligibleHeaderDecls env @@ -412,7 +415,7 @@ private def idCompletionCore match openDecl with | OpenDecl.explicit openedId resolvedId => if allowCompletion eligibleHeaderDecls env resolvedId then - if let some score := matchAtomic id openedId then + if let some score := matchAtomic id openedId danglingDot then addUnresolvedCompletionItemForDecl (.mkSimple openedId.getString!) resolvedId score | OpenDecl.simple ns _ => getAliasState env |>.forM fun alias declNames => do @@ -430,11 +433,12 @@ private def idCompletionCore | _ => return () searchAlias ctx.currNamespace -- Search keywords - if let .str .anonymous s := id then - let keywords := Parser.getTokenTable env - for keyword in keywords.findPrefix s do - if let some score := fuzzyMatchScoreWithThreshold? s keyword then - addKeywordCompletionItem keyword score + if !danglingDot then + if let .str .anonymous s := id then + let keywords := Parser.getTokenTable env + for keyword in keywords.findPrefix s do + if let some score := fuzzyMatchScoreWithThreshold? s keyword then + addKeywordCompletionItem keyword score -- Search namespaces completeNamespaces ctx id danglingDot diff --git a/tests/lean/interactive/completionDanglingDot.lean b/tests/lean/interactive/completionDanglingDot.lean new file mode 100644 index 000000000000..26cd441b359f --- /dev/null +++ b/tests/lean/interactive/completionDanglingDot.lean @@ -0,0 +1,12 @@ +-- Regression test for a bug where the dangling dot was not accounted for in some +-- atomic completions, which lead to invalid completions after a dangling dot + +def foo : Unit := + x. -- No completions expected + --^ textDocument/completion + +def bar : Array Nat := Id.run do + let mut x := sorry + let foo := x. -- No completions expected + --^ textDocument/completion + sorry diff --git a/tests/lean/interactive/completionDanglingDot.lean.expected.out b/tests/lean/interactive/completionDanglingDot.lean.expected.out new file mode 100644 index 000000000000..3932c84d1cb8 --- /dev/null +++ b/tests/lean/interactive/completionDanglingDot.lean.expected.out @@ -0,0 +1,6 @@ +{"textDocument": {"uri": "file:///completionDanglingDot.lean"}, + "position": {"line": 4, "character": 4}} +{"items": [], "isIncomplete": true} +{"textDocument": {"uri": "file:///completionDanglingDot.lean"}, + "position": {"line": 9, "character": 15}} +{"items": [], "isIncomplete": true}