f401f73 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

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

794 Build-depends: idris

795 , base

796 , filepath

797+ , directory

797 , haskeline >= 0.7

798 , haskeline >= 0.7

798 , transformers

799 , transformers

799

800

main/Main.hs+7

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

5import System.Environment

6import System.Exit

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

8+import System.Directory

8

9

9import Data.Maybe

10import Data.Maybe

10import Data.Version

11import Data.Version

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

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

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

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

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

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

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

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

48 case opt getClient opts of

50 case opt getClient opts of

49 [] -> return ()

51 [] -> return ()

50 (c:_) -> do setVerbose False

52 (c:_) -> do setVerbose False

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

92showIncs = do incFlags <- getIncFlags

94showIncs = do incFlags <- getIncFlags

93 putStrLn $ unwords incFlags

95 putStrLn $ unwords incFlags

94 exitWith ExitSuccess

96 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

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

388 | ShowLibs

389 | ShowLibdir

390 | ShowIncs

391+ | ShowPkgs

391 | NoBasePkgs

392 | NoBasePkgs

392 | NoPrelude

393 | NoPrelude

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

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

src/Idris/CmdOptions.hs+1

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Completion.hs+9

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

4import Idris.Core.Evaluate (ctxtAlist)

5import Idris.Core.TT

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

151+ completeArg _ = noCompletion (prev, next)

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

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

149

153

150-- | Complete REPL commands and defined identifiers

154-- | Complete REPL commands and defined identifiers

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

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

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

156

160

157

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+

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

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

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

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

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

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

src/Idris/Imports.hs+20

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

1module Idris.Imports where

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+