@@ -29,6 +29,8 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
29 | ExprTArg
29 | ExprTArg
30 | AltsTArg
30 | AltsTArg
32+-- The FIXMEs are Issue #1766 in the issue tracker.
33+-- https://github.com/idris-lang/Idris-dev/issues/1766
32-- | A list of available tactics and their argument requirements
34-- | A list of available tactics and their argument requirements
33tacticArgs :: [(String, Maybe TacticArg)]
35tacticArgs :: [(String, Maybe TacticArg)]
34tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
36tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
@@ -67,6 +69,8 @@ nameString (NS n _) = nameString n
67nameString _ = Nothing
69nameString _ = Nothing
69-- FIXME: Respect module imports
71-- FIXME: Respect module imports
72+-- Issue #1767 in the issue tracker.
73+-- https://github.com/idris-lang/Idris-dev/issues/1767
70-- | Get the user-visible names from the current interpreter state.
74-- | Get the user-visible names from the current interpreter state.
71names :: Idris [String]
75names :: Idris [String]
72names = do i <- get
76names = do i <- get
@@ -156,6 +160,8 @@ completeColour (prev, next) = case words (reverse prev) of
156 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
160 completeColourFormat = let getCmpl = completeWith (colours ++ formats) in
157 completeWord Nothing " \t" (return . getCmpl)
161 completeWord Nothing " \t" (return . getCmpl)
163+-- The FIXMEs are Issue #1768 on the issue tracker.
164+-- https://github.com/idris-lang/Idris-dev/issues/1768
159-- | Get the completion function for a particular command
165-- | Get the completion function for a particular command
160completeCmd :: String -> CompletionFunc Idris
166completeCmd :: String -> CompletionFunc Idris
161completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
167completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
@@ -183,6 +189,8 @@ replCompletion (prev, next) = case firstWord of
183 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
189 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
192+-- The TODOs are Issue #1769 on the issue tracker.
193+-- https://github.com/idris-lang/Idris-dev/issues/1769
186completeTactic :: [String] -> String -> CompletionFunc Idris
194completeTactic :: [String] -> String -> CompletionFunc Idris
187completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
195completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $
188 lookup tac tacticArgs
196 lookup tac tacticArgs