c1cf03f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commitc1cf03fa7c2abd09f41ad2fc14a6c47d9eda3d71 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 3 Jan 2015, 11:41 (12 years ago) parent2ec25c2 f401f73

6 files changed+39

compare with master

unifiedsplit

idris.cabal+1 main/Main.hs+7 src/Idris/AbsSyntaxTree.hs+1 src/Idris/CmdOptions.hs+1 src/Idris/Completion.hs+9 src/Idris/Imports.hs+20

idris.cabal+1

@@ -794,6 +794,7 @@ Executable idris

794794 Build-depends: idris

795795 , base

796796 , filepath

797+ , directory

797798 , haskeline >= 0.7

798799 , transformers

799800

main/Main.hs+7

@@ -5,6 +5,7 @@ import System.IO

55import System.Environment

66import System.Exit

77import System.FilePath ((</>), addTrailingPathSeparator)

8+import System.Directory

910import Data.Maybe

1011import Data.Version

@@ -45,6 +46,7 @@ runIdris opts = do

4546 when (ShowIncs `elem` opts) $ runIO showIncs

4647 when (ShowLibs `elem` opts) $ runIO showLibs

4748 when (ShowLibdir `elem` opts) $ runIO showLibdir

49+ when (ShowPkgs `elem` opts) $ runIO showPkgs

4850 case opt getClient opts of

4951 [] -> return ()

5052 (c:_) -> do setVerbose False

@@ -92,3 +94,8 @@ showIncs :: IO b

9294showIncs = do incFlags <- getIncFlags

9395 putStrLn $ unwords incFlags

9496 exitWith ExitSuccess

97+

98+-- | List idris packages installed

99+showPkgs :: IO b

100+showPkgs = do mapM putStrLn =<< installedPackages

101+ exitWith ExitSuccess

src/Idris/AbsSyntaxTree.hs+1

@@ -391,6 +391,7 @@ data Opt = Filename String

391391 | ShowLibs

392392 | ShowLibdir

393393 | ShowIncs

394+ | ShowPkgs

394395 | NoBasePkgs

395396 | NoPrelude

396397 | NoBuiltins -- only for the really primitive stuff!

src/Idris/CmdOptions.hs+1

@@ -89,6 +89,7 @@ parseFlags = many $

8989 <|> flag' NoCoverage (long "nocoverage")

9090 <|> flag' ErrContext (long "errorcontext")

9191 <|> flag' ShowLibs (long "link" <> help "Display link flags")

92+ <|> flag' ShowPkgs (long "listlibs" <> help "Display installed libraries")

9293 <|> flag' ShowLibdir (long "libdir" <> help "Display library directory")

9394 <|> flag' ShowIncs (long "include" <> help "Display the includes flags")

9495 <|> flag' Verbose (short 'V' <> long "verbose" <> help "Loud verbosity")

src/Idris/Completion.hs+9

@@ -4,8 +4,10 @@ module Idris.Completion (replCompletion, proverCompletion) where

44import Idris.Core.Evaluate (ctxtAlist)

55import Idris.Core.TT

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,9 +144,11 @@ 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

151+ completeArg _ = noCompletion (prev, next)

148152 completeCmdName = return $ ("", completeWith commands cmd)

149153

150154-- | Complete REPL commands and defined identifiers

@@ -155,6 +159,11 @@ replCompletion (prev, next) = case firstWord of

155159 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev

156160

157161

162+completePkg :: CompletionFunc Idris

163+completePkg = completeWord Nothing " \t()" completeP

164+ where completeP p = do pkgs <- runIO installedPackages

165+ return $ completeWith pkgs p

166+

158167-- The TODOs are Issue #1769 on the issue tracker.

159168-- https://github.com/idris-lang/Idris-dev/issues/1769

160169completeTactic :: [String] -> String -> CompletionFunc Idris

src/Idris/Imports.hs+20

@@ -1,10 +1,15 @@

11module Idris.Imports where

3+import Control.Applicative ((<$>))

4+import Data.List (isSuffixOf)

36import Idris.AbsSyntax

47import Idris.Error

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+