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.
commitcfdcec557ddf2f59cef291d3d3a059c4de9aca18
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 12 Mar 2013, 17:24 (14 years ago)
parent6f194a2
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