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