@@ -0,0 +1,49 @@
1+module Idris.Completion (idrisCompletion) where
3+import Core.Evaluate (ctxtAlist)
6+import Idris.AbsSyntaxTree
8+import Control.Monad.State.Strict
13+import System.Console.Haskeline
16+-- | Convert a name into a string usable for completion. Filters out names
17+-- that users probably don't want to see.
18+nameString :: Name -> Maybe String
19+nameString (UN ('@':_)) = Nothing
20+nameString (UN ('#':_)) = Nothing
21+nameString (UN n) = Just n
22+nameString (NS n _) = nameString n
23+nameString _ = Nothing
25+-- FIXME: Respect module imports
26+-- | Get the user-visible names from the current interpreter state.
27+names :: StateT IState IO [String]
30+ return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
32+completeWith :: [String] -> String -> (String, [Completion])
33+completeWith ns n = if uniqueExists
34+ then ("", [simpleCompletion n])
35+ else ("", map simpleCompletion prefixMatches)
36+ where prefixMatches = filter (isPrefixOf n) ns
37+ uniqueExists = n `elem` prefixMatches
40+idrisCompletion :: [String] -> CompletionFunc (StateT IState IO)
41+idrisCompletion commands (before, after) = complete (reverse $ dropWhile (\x -> x == ' ') before)
42+ where complete :: String -> StateT IState IO (String, [Completion])
43+ complete [] = noCompletions
44+ complete (':':cmd) = return $ completeWith commands (':':cmd)
45+ complete n = do { ns <- names ; return $ completeWith ns n }
47+ noCompletions = return (before, [])