git.iko.soy/Idris-dev
on master help sign in
Add function to list installed packages

Additionally, add (rough) REPL completion for packages

commiteffc954de101c93f5ede949cd4fa714685774391 authorBen Sherman <sherman@metsci.com> dateFri 2 Jan 2015, 18:49 (12 years ago) parentd31f30f
2 files changed+28
compare with master
unifiedsplit
src/Idris/Completion.hs+8 src/Idris/Imports.hs+20
src/Idris/Completion.hs+8
@@ -4,8 +4,10 @@ module Idris.Completion (replCompletion, proverCompletion) where
44import Idris.Core.Evaluate (ctxtAlist)
55import Idris.Core.TT
66
7+import Idris.AbsSyntax (runIO)
78import Idris.AbsSyntaxTree
89import Idris.Help
10+import Idris.Imports (installedPackages)
911import Idris.Colours
1012import Idris.ParseHelpers(opChars)
1113import qualified Idris.ParseExpr (constants, tactics)
@@ -142,6 +144,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo
142144 completeArg NoArg = noCompletion (prev, next)
143145 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)
144146 completeArg DeclArg = completeExpr [] (prev, next)
147+ completeArg PkgArgs = completePkg (prev, next)
145148 completeArg (ManyArgs a) = completeArg a
146149 completeArg (OptionalArg a) = completeArg a
147150 completeArg (SeqArgs a b) = completeArg a
@@ -156,6 +159,11 @@ replCompletion (prev, next) = case firstWord of
156159 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
157160
158161
162+completePkg :: CompletionFunc Idris
163+completePkg = completeWord Nothing " \t()" completeP
164+ where completeP p = do pkgs <- runIO installedPackages
165+ return $ completeWith pkgs p
166+
159167-- The TODOs are Issue #1769 on the issue tracker.
160168-- https://github.com/idris-lang/Idris-dev/issues/1769
161169completeTactic :: [String] -> String -> CompletionFunc Idris
src/Idris/Imports.hs+20
@@ -1,10 +1,15 @@
11module Idris.Imports where
22
3+import Control.Applicative ((<$>))
4+import Data.List (isSuffixOf)
5+
36import Idris.AbsSyntax
47import Idris.Error
58
69import Idris.Core.TT
710
11+import IRTS.System (getIdrisLibDir)
12+
813import System.FilePath
914import System.Directory
1015import Control.Monad.State.Strict
@@ -81,3 +86,18 @@ findPkgIndex p = do let idx = pkgIndex p
8186 ids <- allImportDirs
8287 runIO $ findInPath ids idx
8388
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+