@@ -12,6 +12,39 @@ import Data.Maybe
1212
1313import System.Console.Haskeline
1414
15+-- TODO: add specific classes of identifiers to complete, fx metavariables
16+-- | A specification of the arguments that REPL commands can take
17+data CmdArg = ExprArg -- ^ The command takes an expression
18+ | NameArg -- ^ The command takes a name
19+ | FileArg -- ^ The command takes a file
20+ | ModuleArg -- ^ The command takes a module name
21+ | OptionArg -- ^ The command takes an option
22+
23+-- | Information about how to complete the various commands
24+cmdArgs :: [(String, CmdArg)]
25+cmdArgs = [ (":t", ExprArg)
26+ , (":miss", NameArg)
27+ , (":missing", NameArg)
28+ , (":i", NameArg)
29+ , (":info", NameArg)
30+ , (":total", NameArg)
31+ , (":l", FileArg)
32+ , (":load", FileArg)
33+ , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
34+ , (":p", NameArg)
35+ , (":prove", NameArg)
36+ , (":a", NameArg)
37+ , (":addproof", NameArg)
38+ , (":rmproof", NameArg)
39+ , (":showproof", NameArg)
40+ , (":c", FileArg)
41+ , (":compile", FileArg)
42+ , (":js", FileArg)
43+ , (":javascript", FileArg)
44+ , (":set", OptionArg)
45+ , (":unset", OptionArg)
46+ ]
47+commands = map fst cmdArgs
1548
1649-- | Convert a name into a string usable for completion. Filters out names
1750-- that users probably don't want to see.
@@ -29,6 +62,11 @@ names = do i <- get
2962 let ctxt = tt_ctxt i
3063 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
3164
65+
66+modules :: StateT IState IO [String]
67+modules = do i <- get
68+ return $ map show $ imported i
69+
3270completeWith :: [String] -> String -> [Completion]
3371completeWith ns n = if uniqueExists
3472 then [simpleCompletion n]
@@ -41,15 +79,27 @@ completeName n = do ns <- names
4179 return $ completeWith ns n
4280
4381completeExpr :: CompletionFunc (StateT IState IO)
44−completeExpr = completeWord Nothing [' ', '\t'] completeName
82+completeExpr = completeWord Nothing " \t" completeName
4583
46−idrisCompletion :: [String] -> CompletionFunc (StateT IState IO)
47−idrisCompletion commands (before, after) = complete (reverse $ dropWhile (\x -> x == ' ') before)
48− where complete :: String -> StateT IState IO (String, [Completion])
49− complete [] = noCompletions
50− complete (':':cmd) = return $ ("", completeWith commands (':':cmd))
51− complete _ = completeExpr (before, after)
84+completeOption :: CompletionFunc (StateT IState IO)
85+completeOption = completeWord Nothing " \t" completeOpt
86+ where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
5287
53− noCompletions = return (before, [])
88+isWhitespace :: Char -> Bool
89+isWhitespace = (flip elem) " \t\n"
5490
91+-- | Get the completion function for a particular command
92+completeCmd :: String -> CompletionFunc (StateT IState IO)
93+completeCmd cmd (prev, next) = fromMaybe completeCmdName (fmap completeArg $ lookup cmd cmdArgs)
94+ where completeArg FileArg = completeFilename (prev, next)
95+ completeArg NameArg = completeExpr (prev, next) -- FIXME only complete one name
96+ completeArg OptionArg = completeOption (prev, next)
97+ completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
98+ completeArg ExprArg = completeExpr (prev, next)
99+ completeCmdName = return $ ("", completeWith commands cmd)
55100
101+idrisCompletion :: CompletionFunc (StateT IState IO)
102+idrisCompletion (prev, next) = case firstWord of
103+ ':':cmdName -> completeCmd (':':cmdName) (prev, next)
104+ _ -> completeExpr (prev, next)
105+ where (firstWord, remainder) = break isWhitespace $ dropWhile isWhitespace $ reverse prev