@@ -0,0 +1,49 @@
1+module Idris.Completion (idrisCompletion) where
2+
3+import Core.Evaluate (ctxtAlist)
4+import Core.TT
5+
6+import Idris.AbsSyntaxTree
7+
8+import Control.Monad.State.Strict
9+
10+import Data.List
11+import Data.Maybe
12+
13+import System.Console.Haskeline
14+
15+
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
24+
25+-- FIXME: Respect module imports
26+-- | Get the user-visible names from the current interpreter state.
27+names :: StateT IState IO [String]
28+names = do i <- get
29+ let ctxt = tt_ctxt i
30+ return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
31+
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
38+
39+
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 }
46+
47+ noCompletions = return (before, [])
48+
49+