Stop completion of names that are prefixes of others
Previously, when completing "plus", it was accepted. Now, it tries completing
with "plusAssociative", "plusCommutative", etc, and the user has to press
space.
commit1617dd36a60a438322e0f1b2678bc9c37f3e04bd
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 12 Mar 2013, 17:24 (14 years ago)
parent25a4649
src/Idris/Completion.hs+1−1
@@ -103,7 +103,7 @@ completeWith ns n = if uniqueExists
103103 then [simpleCompletion n]
104104 else map simpleCompletion prefixMatches
105105 where prefixMatches = filter (isPrefixOf n) ns
106− uniqueExists = n `elem` prefixMatches
106+ uniqueExists = [n] == prefixMatches
107107
108108completeName :: [String] -> String -> Idris [Completion]
109109completeName extra n = do ns <- names