@@ -29,20 +29,26 @@ names = do i <- get
29 let ctxt = tt_ctxt i
29 let ctxt = tt_ctxt i
30 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
30 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
32−completeWith :: [String] -> String -> (String, [Completion])
32+completeWith :: [String] -> String -> [Completion]
33completeWith ns n = if uniqueExists
33completeWith ns n = if uniqueExists
34− then ("", [simpleCompletion n])
34+ then [simpleCompletion n]
35− else ("", map simpleCompletion prefixMatches)
35+ else map simpleCompletion prefixMatches
36 where prefixMatches = filter (isPrefixOf n) ns
36 where prefixMatches = filter (isPrefixOf n) ns
37 uniqueExists = n `elem` prefixMatches
37 uniqueExists = n `elem` prefixMatches
39+completeName :: String -> StateT IState IO [Completion]
40+completeName n = do ns <- names
41+ return $ completeWith ns n
43+completeExpr :: CompletionFunc (StateT IState IO)
44+completeExpr = completeWord Nothing [' ', '\t'] completeName
40idrisCompletion :: [String] -> CompletionFunc (StateT IState IO)
46idrisCompletion :: [String] -> CompletionFunc (StateT IState IO)
41idrisCompletion commands (before, after) = complete (reverse $ dropWhile (\x -> x == ' ') before)
47idrisCompletion commands (before, after) = complete (reverse $ dropWhile (\x -> x == ' ') before)
42 where complete :: String -> StateT IState IO (String, [Completion])
48 where complete :: String -> StateT IState IO (String, [Completion])
43 complete [] = noCompletions
49 complete [] = noCompletions
44− complete (':':cmd) = return $ completeWith commands (':':cmd)
50+ complete (':':cmd) = return $ ("", completeWith commands (':':cmd))
45− complete n = do { ns <- names ; return $ completeWith ns n }
51+ complete _ = completeExpr (before, after)
47 noCompletions = return (before, [])
53 noCompletions = return (before, [])