@@ -1,3 +1,4 @@
1+-- | Support for command-line completion at the REPL and in the prover
1module Idris.Completion (replCompletion, proverCompletion) where
2module Idris.Completion (replCompletion, proverCompletion) where
3import Core.Evaluate (ctxtAlist)
4import Core.Evaluate (ctxtAlist)
@@ -122,6 +123,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
122 completeArg ExprArg = completeExpr [] (prev, next)
123 completeArg ExprArg = completeExpr [] (prev, next)
123 completeCmdName = return $ ("", completeWith commands cmd)
124 completeCmdName = return $ ("", completeWith commands cmd)
126+-- | Complete REPL commands and defined identifiers
125replCompletion :: CompletionFunc Idris
127replCompletion :: CompletionFunc Idris
126replCompletion (prev, next) = case firstWord of
128replCompletion (prev, next) = case firstWord of
127 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
129 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
@@ -137,7 +139,8 @@ completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeAr
137 completeArg (Just ExprTArg) = completeExpr as (prev, next)
139 completeArg (Just ExprTArg) = completeExpr as (prev, next)
138 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
140 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
140−
142+-- | Complete tactics and their arguments
143+proverCompletion :: [String] -- ^ The names of current local assumptions
141−proverCompletion :: [String] -> CompletionFunc Idris
144+ -> CompletionFunc Idris
142proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
145proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
143 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
146 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev