@@ -21,6 +21,7 @@ data CmdArg = ExprArg -- ^ The command takes an expression
21 | FileArg -- ^ The command takes a file
21 | FileArg -- ^ The command takes a file
22 | ModuleArg -- ^ The command takes a module name
22 | ModuleArg -- ^ The command takes a module name
23 | OptionArg -- ^ The command takes an option
23 | OptionArg -- ^ The command takes an option
24+ | MetaVarArg -- ^ The command takes a metavariable
25-- | Information about how to complete the various commands
26-- | Information about how to complete the various commands
26cmdArgs :: [(String, CmdArg)]
27cmdArgs :: [(String, CmdArg)]
@@ -33,8 +34,8 @@ cmdArgs = [ (":t", ExprArg)
33 , (":l", FileArg)
34 , (":l", FileArg)
34 , (":load", FileArg)
35 , (":load", FileArg)
35 , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
36 , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
36− , (":p", NameArg)
37+ , (":p", MetaVarArg)
37− , (":prove", NameArg)
38+ , (":prove", MetaVarArg)
38 , (":a", NameArg)
39 , (":a", NameArg)
39 , (":addproof", NameArg)
40 , (":addproof", NameArg)
40 , (":rmproof", NameArg)
41 , (":rmproof", NameArg)
@@ -81,11 +82,15 @@ nameString _ = Nothing
82-- FIXME: Respect module imports
83-- FIXME: Respect module imports
83-- | Get the user-visible names from the current interpreter state.
84-- | Get the user-visible names from the current interpreter state.
84−names :: Idris[String]
85+names :: Idris [String]
85names = do i <- get
86names = do i <- get
86 let ctxt = tt_ctxt i
87 let ctxt = tt_ctxt i
87 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
88 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
90+metavars :: Idris [String]
91+metavars = do i <- get
92+ return . map (show . nsroot) $ idris_metavars i \\ primDefs
90modules :: Idris [String]
95modules :: Idris [String]
91modules = do i <- get
96modules = do i <- get
@@ -107,6 +112,11 @@ completeName extra n = do ns <- names
107completeExpr :: [String] -> CompletionFunc Idris
112completeExpr :: [String] -> CompletionFunc Idris
108completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
113completeExpr extra = completeWord Nothing (" \t(){}:" ++ opChars) (completeName extra)
115+completeMetaVar :: CompletionFunc Idris
116+completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM
117+ where completeM m = do mvs <- metavars
118+ return $ completeWith mvs m
110completeOption :: CompletionFunc Idris
120completeOption :: CompletionFunc Idris
111completeOption = completeWord Nothing " \t" completeOpt
121completeOption = completeWord Nothing " \t" completeOpt
112 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
122 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
@@ -122,6 +132,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
122 completeArg OptionArg = completeOption (prev, next)
132 completeArg OptionArg = completeOption (prev, next)
123 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
133 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
124 completeArg ExprArg = completeExpr [] (prev, next)
134 completeArg ExprArg = completeExpr [] (prev, next)
135+ completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
125 completeCmdName = return $ ("", completeWith commands cmd)
136 completeCmdName = return $ ("", completeWith commands cmd)
127-- | Complete REPL commands and defined identifiers
138-- | Complete REPL commands and defined identifiers