git.iko.soy/Idris-dev
on master help sign in
Add function to list installed packages
effc954Ben Sherman
src/Idris/Completion.hs+8
compare with master
unifiedsplit
@@ -4,8 +4,10 @@ module Idris.Completion (replCompletion, proverCompletion) where
4import Idris.Core.Evaluate (ctxtAlist)
4import Idris.Core.Evaluate (ctxtAlist)
5import Idris.Core.TT
5import Idris.Core.TT
6
6
7+import Idris.AbsSyntax (runIO)
7import Idris.AbsSyntaxTree
8import Idris.AbsSyntaxTree
8import Idris.Help
9import Idris.Help
10+import Idris.Imports (installedPackages)
9import Idris.Colours
11import Idris.Colours
10import Idris.ParseHelpers(opChars)
12import Idris.ParseHelpers(opChars)
11import qualified Idris.ParseExpr (constants, tactics)
13import qualified Idris.ParseExpr (constants, tactics)
@@ -142,6 +144,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
142 completeArg NoArg = noCompletion (prev, next)
144 completeArg NoArg = noCompletion (prev, next)
143 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
145 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
144 completeArg DeclArg = completeExpr [] (prev, next)
146 completeArg DeclArg = completeExpr [] (prev, next)
147+ completeArg PkgArgs = completePkg (prev, next)
145 completeArg (ManyArgs a) = completeArg a
148 completeArg (ManyArgs a) = completeArg a
146 completeArg (OptionalArg a) = completeArg a
149 completeArg (OptionalArg a) = completeArg a
147 completeArg (SeqArgs a b) = completeArg a
150 completeArg (SeqArgs a b) = completeArg a
@@ -156,6 +159,11 @@ replCompletion (prev, next) = case firstWord of
156 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
159 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
157
160
158
161
162+completePkg :: CompletionFunc Idris
163+completePkg = completeWord Nothing " \t()" completeP
164+ where completeP p = do pkgs <- runIO installedPackages
165+ return $ completeWith pkgs p
166+
159-- The TODOs are Issue #1769 on the issue tracker.
167-- The TODOs are Issue #1769 on the issue tracker.
160-- https://github.com/idris-lang/Idris-dev/issues/1769
168-- https://github.com/idris-lang/Idris-dev/issues/1769
161completeTactic :: [String] -> String -> CompletionFunc Idris
169completeTactic :: [String] -> String -> CompletionFunc Idris
src/Idris/Imports.hs+20
@@ -1,10 +1,15 @@
1module Idris.Imports where
1module Idris.Imports where
2
2
3+import Control.Applicative ((<$>))
4+import Data.List (isSuffixOf)
5+
3import Idris.AbsSyntax
6import Idris.AbsSyntax
4import Idris.Error
7import Idris.Error
5
8
6import Idris.Core.TT
9import Idris.Core.TT
7
10
11+import IRTS.System (getIdrisLibDir)
12+
8import System.FilePath
13import System.FilePath
9import System.Directory
14import System.Directory
10import Control.Monad.State.Strict
15import Control.Monad.State.Strict
@@ -81,3 +86,18 @@ findPkgIndex p = do let idx = pkgIndex p
81 ids <- allImportDirs
86 ids <- allImportDirs
82 runIO $ findInPath ids idx
87 runIO $ findInPath ids idx
83
88
89+
90+installedPackages :: IO [String]
91+installedPackages = do
92+ idir <- getIdrisLibDir
93+ filterM (goodDir idir) =<< dirContents idir
94+ where
95+ allFilesInDir base fp = do
96+ let fullpath = base </> fp
97+ isDir <- doesDirectoryExist fullpath
98+ if isDir
99+ then fmap concat (mapM (allFilesInDir fullpath) =<< dirContents fullpath)
100+ else return [fp]
101+ dirContents = fmap (filter (not . (`elem` [".", ".."]))) . getDirectoryContents
102+ goodDir idir d = any (".ibc" `isSuffixOf`) <$> allFilesInDir idir d
103+