65ee53e · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+13

compare with master

unifiedsplit

@@ -9,6 +9,7 @@ import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10import Idris.AbsSyntaxTree

11import Idris.IdeSlave

12+import Idris.Colours

12import IRTS.CodegenCommon

13import IRTS.CodegenCommon

13import Util.DynamicLinker

14import Util.DynamicLinker

14

15

@@ -506,6 +507,18 @@ setImpShow t = do i <- getIState

506 let opt' = opts { opt_showimp = t }

507 let opt' = opts { opt_showimp = t }

507 putIState $ i { idris_options = opt' }

508 putIState $ i { idris_options = opt' }

508

509

510+setColour :: ColourType -> IdrisColour -> Idris ()

511+setColour ct c = do i <- getIState

512+ let newTheme = setColour' ct c (idris_colourTheme i)

513+ putIState $ i { idris_colourTheme = newTheme }

514+ where setColour' KeywordColour c t = t { keywordColour = c }

515+ setColour' BoundVarColour c t = t { boundVarColour = c }

516+ setColour' ImplicitColour c t = t { implicitColour = c }

517+ setColour' FunctionColour c t = t { functionColour = c }

518+ setColour' TypeColour c t = t { typeColour = c }

519+ setColour' DataColour c t = t { dataColour = c }

520+ setColour' PromptColour c t = t { promptColour = c }

521+

509logLvl :: Int -> String -> Idris ()

522logLvl :: Int -> String -> Idris ()

510logLvl l str = do i <- getIState

523logLvl l str = do i <- getIState

511 let lvl = opt_logLevel (idris_options i)

524 let lvl = opt_logLevel (idris_options i)

src/Idris/AbsSyntaxTree.hs+3

@@ -235,6 +235,9 @@ data Command = Quit

235 | SetOpt Opt

236 | UnsetOpt Opt

237 | NOP

238+ | SetColour ColourType IdrisColour

239+ | ColourOn

240+ | ColourOff

238

241

239data Opt = Filename String

242data Opt = Filename String

240 | Ver

243 | Ver

src/Idris/Colours.hs+21−2

@@ -3,7 +3,9 @@ module Idris.Colours (

3 ColourTheme(..),

4 defaultTheme,

5 colouriseKwd, colouriseBound, colouriseImplicit,

6− colouriseType, colouriseFun, colouriseData) where

6+ colouriseType, colouriseFun, colouriseData,

7+ colourisePrompt,

8+ ColourType(..)) where

7

9

8import System.Console.ANSI

10import System.Console.ANSI

9

11

@@ -12,6 +14,7 @@ data IdrisColour = IdrisColour { colour :: Color

12 , underline :: Bool

14 , underline :: Bool

13 , bold :: Bool

15 , bold :: Bool

14 }

16 }

17+ deriving (Eq, Show)

15

18

16mkColour :: Color -> IdrisColour

19mkColour :: Color -> IdrisColour

17mkColour c = IdrisColour c True False False

20mkColour c = IdrisColour c True False False

@@ -22,7 +25,9 @@ data ColourTheme = ColourTheme { keywordColour :: IdrisColour

22 , functionColour :: IdrisColour

25 , functionColour :: IdrisColour

23 , typeColour :: IdrisColour

26 , typeColour :: IdrisColour

24 , dataColour :: IdrisColour

27 , dataColour :: IdrisColour

28+ , promptColour :: IdrisColour

25 }

29 }

30+ deriving (Eq, Show)

26

31

27defaultTheme :: ColourTheme

32defaultTheme :: ColourTheme

28defaultTheme = ColourTheme { keywordColour = IdrisColour Black True True True

33defaultTheme = ColourTheme { keywordColour = IdrisColour Black True True True

@@ -31,6 +36,7 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Black True True True

31 , functionColour = mkColour Green

36 , functionColour = mkColour Green

32 , typeColour = mkColour Blue

37 , typeColour = mkColour Blue

33 , dataColour = mkColour Red

38 , dataColour = mkColour Red

39+ , promptColour = IdrisColour Black True False True

34 }

40 }

35

41

36-- Set the colour of a string using POSIX escape codes

42-- Set the colour of a string using POSIX escape codes

@@ -56,4 +62,17 @@ colouriseType :: ColourTheme -> String -> String

56colouriseType t = colourise (typeColour t)

62colouriseType t = colourise (typeColour t)

57

63

58colouriseData :: ColourTheme -> String -> String

64colouriseData :: ColourTheme -> String -> String

59−colouriseData t = colourise (dataColour t)

65+colouriseData t = colourise (dataColour t)

66+

67+colourisePrompt :: ColourTheme -> String -> String

68+colourisePrompt t = colourise (promptColour t)

69+

70+

71+data ColourType = KeywordColour

72+ | BoundVarColour

73+ | ImplicitColour

74+ | FunctionColour

75+ | TypeColour

76+ | DataColour

77+ | PromptColour

78+ deriving (Eq, Show, Bounded, Enum)

src/Idris/Completion.hs+30

@@ -7,13 +7,16 @@ import Core.CoreParser (opChars)

7

8import Idris.AbsSyntaxTree

9import Idris.Help

10+import Idris.Colours

10

11

11import Control.Monad.State.Strict

12import Control.Monad.State.Strict

12

13

13import Data.List

14import Data.List

14import Data.Maybe

15import Data.Maybe

16+import Data.Char(toLower)

15

17

16import System.Console.Haskeline

18import System.Console.Haskeline

19+import System.Console.ANSI (Color)

17

20

18

21

19fst3 :: (a, b, c) -> a

22fst3 :: (a, b, c) -> a

@@ -109,6 +112,32 @@ lookupInHelp cmd = lookupInHelp' cmd help

109 | otherwise = lookupInHelp' cmd xs

112 | otherwise = lookupInHelp' cmd xs

110 lookupInHelp' cmd [] = Nothing

113 lookupInHelp' cmd [] = Nothing

111

114

115+completeColour :: CompletionFunc Idris

116+completeColour (prev, next) = case words (reverse prev) of

117+ [c] | isCmd c -> do cmpls <- completeColourOpt next

118+ return (reverse $ c ++ " ", cmpls)

119+ [c, o] | o `elem` opts -> let correct = (c ++ " " ++ o) in

120+ return (reverse correct, [simpleCompletion ""])

121+ | o `elem` colourTypes -> completeColourFormat (prev, next)

122+ | otherwise -> let cmpls = completeWith (opts ++ colourTypes) o in

123+ let sofar = (c ++ " ") in

124+ return (reverse sofar, cmpls)

125+ cmd@(c:o:_) | isCmd c && o `elem` colourTypes ->

126+ completeColourFormat (prev, next)

127+ _ -> noCompletion (prev, next)

128+ where completeColourOpt :: String -> Idris [Completion]

129+ completeColourOpt = return . completeWith (opts ++ colourTypes)

130+ opts = ["on", "off"]

131+ colourTypes = map (map toLower . reverse . drop 6 . reverse . show) $

132+ enumFromTo (minBound::ColourType) maxBound

133+ isCmd ":colour" = True

134+ isCmd ":color" = True

135+ isCmd _ = False

136+ colours = map (map toLower . show) $ enumFromTo (minBound::Color) maxBound

137+ formats = ["vivid", "dull", "underline", "nounderline", "bold", "nobold"]

138+ completeColourFormat = let getCmpl = completeWith (colours ++ formats) in

139+ completeWord Nothing " \t" (return . getCmpl)

140+

112-- | Get the completion function for a particular command

141-- | Get the completion function for a particular command

113completeCmd :: String -> CompletionFunc Idris

142completeCmd :: String -> CompletionFunc Idris

114completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd

143completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd

@@ -118,6 +147,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo

118 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

147 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later

119 completeArg ExprArg = completeExpr [] (prev, next)

148 completeArg ExprArg = completeExpr [] (prev, next)

120 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

149 completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name

150+ completeArg ColourArg = completeColour (prev, next)

121 completeArg NoArg = noCompletion (prev, next)

151 completeArg NoArg = noCompletion (prev, next)

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

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

123

153

src/Idris/Help.hs+10−7

@@ -6,17 +6,19 @@ data CmdArg = ExprArg -- ^ The command takes an expression

6 | ModuleArg -- ^ The command takes a module name

7 | OptionArg -- ^ The command takes an option

8 | MetaVarArg -- ^ The command takes a metavariable

9+ | ColourArg -- ^ The command is the colour-setting command

9 | NoArg -- ^ No completion (yet!?)

10 | NoArg -- ^ No completion (yet!?)

10 | SpecialHeaderArg -- ^ do not use

11 | SpecialHeaderArg -- ^ do not use

11

12

12instance Show CmdArg where

13instance Show CmdArg where

13− show ExprArg = "<expr>"

14+ show ExprArg = "<expr>"

14− show NameArg = "<name>"

15+ show NameArg = "<name>"

15− show FileArg = "<filename>"

16+ show FileArg = "<filename>"

16− show ModuleArg = "<module>"

17+ show ModuleArg = "<module>"

17− show OptionArg = "<option>"

18+ show OptionArg = "<option>"

18− show MetaVarArg = "<metavar>"

19+ show MetaVarArg = "<metavar>"

20+ show ColourArg = "<option>"

19− show NoArg = ""

21+ show NoArg = ""

20 show SpecialHeaderArg = "Arguments"

22 show SpecialHeaderArg = "Arguments"

21

23

22help :: [([String], CmdArg, String)]

24help :: [([String], CmdArg, String)]

@@ -46,5 +48,6 @@ help =

46 ([":?",":h",":help"], NoArg, "Display this help text"),

48 ([":?",":h",":help"], NoArg, "Display this help text"),

47 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),

49 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),

48 ([":unset"], OptionArg, "Unset an option"),

50 ([":unset"], OptionArg, "Unset an option"),

51+ ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

49 ([":q",":quit"], NoArg, "Exit the Idris system")

52 ([":q",":quit"], NoArg, "Exit the Idris system")

50 ]

53 ]

src/Idris/REPL.hs+12−2

@@ -20,6 +20,7 @@ import Idris.Completion

20import Idris.IdeSlave

21import Idris.Chaser

22import Idris.Imports

23+import Idris.Colours

23

24

24import Paths_idris

25import Paths_idris

25import Util.System

26import Util.System

@@ -68,14 +69,18 @@ repl :: IState -- ^ The initial state

68repl orig mods

69repl orig mods

69 = H.catch

70 = H.catch

70 (do let quiet = opt_quiet (idris_options orig)

71 (do let quiet = opt_quiet (idris_options orig)

72+ i <- lift getIState

73+ let colour = idris_colourRepl i

74+ let theme = idris_colourTheme i

71 let prompt = if quiet

75 let prompt = if quiet

72 then ""

76 then ""

73− else mkPrompt mods ++ "> "

77+ else let str = mkPrompt mods ++ ">" in

78+ (if colour then colourisePrompt theme str else str) ++ " "

74 x <- getInputLine prompt

79 x <- getInputLine prompt

75 case x of

80 case x of

76 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

81 Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")

77 return ()

82 return ()

78− Just input -> H.catch

83+ Just input -> H.catch

79 (do ms <- lift $ processInput input orig mods

84 (do ms <- lift $ processInput input orig mods

80 case ms of

85 case ms of

81 Just mods -> repl orig mods

86 Just mods -> repl orig mods

@@ -541,6 +546,11 @@ process fn (UnsetOpt ShowImpl) = setImpShow False

541

546

542process fn (SetOpt _) = iFail "Not a valid option"

547process fn (SetOpt _) = iFail "Not a valid option"

543process fn (UnsetOpt _) = iFail "Not a valid option"

548process fn (UnsetOpt _) = iFail "Not a valid option"

549+process fn (SetColour ty c) = setColour ty c

550+process fn ColourOn = do ist <- getIState

551+ putIState $ ist { idris_colourRepl = True }

552+process fn ColourOff = do ist <- getIState

553+ putIState $ ist { idris_colourRepl = False }

544

554

545

555

546classInfo :: ClassInfo -> Idris ()

556classInfo :: ClassInfo -> Idris ()

src/Idris/REPLParser.hs+56

@@ -1,7 +1,9 @@

1module Idris.REPLParser(parseCmd) where

2

3import System.FilePath ((</>))

4+import System.Console.ANSI (Color(..))

4

5

6+import Idris.Colours

5import Idris.Parser

7import Idris.Parser

6import Idris.AbsSyntax

8import Idris.AbsSyntax

7import Core.TT

9import Core.TT

@@ -14,6 +16,7 @@ import qualified Text.ParserCombinators.Parsec.Token as PTok

14import Debug.Trace

16import Debug.Trace

15import Data.List

17import Data.List

16import Data.List.Split(splitOn)

18import Data.List.Split(splitOn)

19+import Data.Char(toLower)

17

20

18parseCmd i = runParser pCmd i "(input)"

21parseCmd i = runParser pCmd i "(input)"

19

22

@@ -57,6 +60,7 @@ pCmd = do spaces; try (do cmd ["q", "quit"]; eof; return Quit)

57 <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))

60 <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))

58 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

61 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

59 <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))

62 <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))

63+ <|> try (do cmd ["color", "colour"]; pSetColourCmd)

60 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

64 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

61 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

65 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

62 <|> try (do cmd ["s", "search"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Search t))

66 <|> try (do cmd ["s", "search"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Search t))

@@ -71,3 +75,55 @@ pOption :: IParser Opt

71pOption = do discard (symbol "errorcontext"); return ErrContext

75pOption = do discard (symbol "errorcontext"); return ErrContext

72 <|> do discard (symbol "showimplicits"); return ShowImpl

76 <|> do discard (symbol "showimplicits"); return ShowImpl

73

77

78+

79+colours :: [(String, Color)]

80+colours = [ ("black", Black)

81+ , ("red", Red)

82+ , ("green", Green)

83+ , ("yellow", Yellow)

84+ , ("blue", Blue)

85+ , ("magenta", Magenta)

86+ , ("cyan", Cyan)

87+ , ("white", White)

88+ ]

89+

90+pColour :: IParser Color

91+pColour = doColour colours

92+ where doColour [] = fail "Unknown colour"

93+ doColour ((s, c):cs) = (try (symbol s) >> return c) <|> doColour cs

94+

95+pColourMod :: IParser (IdrisColour -> IdrisColour)

96+pColourMod = try (symbol "vivid" >> return doVivid)

97+ <|> try (symbol "dull" >> return doDull)

98+ <|> try (symbol "underline" >> return doUnderline)

99+ <|> try (symbol "nounderline" >> return doNoUnderline)

100+ <|> try (symbol "bold" >> return doBold)

101+ <|> try (symbol "nobold" >> return doNoBold)

102+ <|> try (pColour >>= return . doSetColour)

103+ where doVivid i = i { vivid = True }

104+ doDull i = i { vivid = False }

105+ doUnderline i = i { underline = True }

106+ doNoUnderline i = i { underline = False }

107+ doBold i = i { bold = True }

108+ doNoBold i = i { bold = False }

109+ doSetColour c i = i { colour = c }

110+

111+

112+colourTypes :: [(String, ColourType)]

113+colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

114+ enumFromTo minBound maxBound

115+

116+pColourType :: IParser ColourType

117+pColourType = doColourType colourTypes

118+ where doColourType [] = fail $ "Unknown colour category. Options: " ++

119+ (concat . intersperse ", " . map fst) colourTypes

120+ doColourType ((s,ct):cts) = (try (symbol s) >> return ct) <|> doColourType cts

121+

122+pSetColourCmd :: IParser Command

123+pSetColourCmd = (do c <- pColourType

124+ let defaultColour = IdrisColour Black True False False

125+ opts <- sepBy pColourMod spaces

126+ let colour = foldr ($) defaultColour $ reverse opts

127+ return $ SetColour c colour)

128+ <|> try (symbol "on" >> return ColourOn)

129+ <|> try (symbol "off" >> return ColourOff)