@@ -21,6 +21,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression
2121 | FileArg -- ^ The command takes a file
2222 | ModuleArg -- ^ The command takes a module name
2323 | OptionArg -- ^ The command takes an option
24+ | MetaVarArg -- ^ The command takes a metavariable
2425
2526-- | Information about how to complete the various commands
2627cmdArgs :: [(String, CmdArg)]
@@ -33,8 +34,8 @@ cmdArgs = [ (":t", ExprArg)
3334 , (":l", FileArg)
3435 , (":load", FileArg)
3536 , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
36− , (":p", NameArg)
37− , (":prove", NameArg)
37+ , (":p", MetaVarArg)
38+ , (":prove", MetaVarArg)
3839 , (":a", NameArg)
3940 , (":addproof", NameArg)
4041 , (":rmproof", NameArg)
@@ -81,11 +82,15 @@ nameString _ = Nothing
8182
8283-- FIXME: Respect module imports
8384-- | Get the user-visible names from the current interpreter state.
84−names :: Idris[String]
85+names :: Idris [String]
8586names = do i <- get
8687 let ctxt = tt_ctxt i
8788 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
8889
90+metavars :: Idris [String]
91+metavars = do i <- get
92+ return . map (show . nsroot) $ idris_metavars i \\ primDefs
93+
8994
9095modules :: Idris [String]
9196modules = do i <- get
@@ -107,6 +112,11 @@ completeName extra n = do ns <- names
107112completeExpr :: [String] -> CompletionFunc Idris
108113completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
109114
115+completeMetaVar :: CompletionFunc Idris
116+completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
117+ where completeM m = do mvs <- metavars
118+ return $ completeWith mvs m
119+
110120completeOption :: CompletionFunc Idris
111121completeOption = completeWord Nothing " \t" completeOpt
112122 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
@@ -122,6 +132,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
122132 completeArg OptionArg = completeOption (prev, next)
123133 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
124134 completeArg ExprArg = completeExpr [] (prev, next)
135+ completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
125136 completeCmdName = return $ ("", completeWith commands cmd)
126137
127138-- | Complete REPL commands and defined identifiers