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

src/Idris/AbsSyntax.hs+13

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

99import Core.Typecheck

1010import Idris.AbsSyntaxTree

1111import Idris.IdeSlave

12+import Idris.Colours

1213import IRTS.CodegenCommon

1314import Util.DynamicLinker

1415

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

506507 let opt' = opts { opt_showimp = t }

507508 putIState $ i { idris_options = opt' }

508509

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+

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

510523logLvl l str = do i <- getIState

511524 let lvl = opt_logLevel (idris_options i)

src/Idris/AbsSyntaxTree.hs+3

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

235235 | SetOpt Opt

236236 | UnsetOpt Opt

237237 | NOP

238+ | SetColour ColourType IdrisColour

239+ | ColourOn

240+ | ColourOff

238241

239242data Opt = Filename String

240243 | Ver

src/Idris/Colours.hs+21−2

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

33 ColourTheme(..),

44 defaultTheme,

55 colouriseKwd, colouriseBound, colouriseImplicit,

6− colouriseType, colouriseFun, colouriseData) where

6+ colouriseType, colouriseFun, colouriseData,

7+ colourisePrompt,

8+ ColourType(..)) where

79

810import System.Console.ANSI

911

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

1214 , underline :: Bool

1315 , bold :: Bool

1416 }

17+ deriving (Eq, Show)

1518

1619mkColour :: Color -> IdrisColour

1720mkColour c = IdrisColour c True False False

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

2225 , functionColour :: IdrisColour

2326 , typeColour :: IdrisColour

2427 , dataColour :: IdrisColour

28+ , promptColour :: IdrisColour

2529 }

30+ deriving (Eq, Show)

2631

2732defaultTheme :: ColourTheme

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

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

3136 , functionColour = mkColour Green

3237 , typeColour = mkColour Blue

3338 , dataColour = mkColour Red

39+ , promptColour = IdrisColour Black True False True

3440 }

3541

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

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

5662colouriseType t = colourise (typeColour t)

5763

5864colouriseData :: 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)

77

88import Idris.AbsSyntaxTree

99import Idris.Help

10+import Idris.Colours

1011

1112import Control.Monad.State.Strict

1213

1314import Data.List

1415import Data.Maybe

16+import Data.Char(toLower)

1517

1618import System.Console.Haskeline

19+import System.Console.ANSI (Color)

1720

1821

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

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

109112 | otherwise = lookupInHelp' cmd xs

110113 lookupInHelp' cmd [] = Nothing

111114

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+

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

113142completeCmd :: String -> CompletionFunc Idris

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

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

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

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

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

150+ completeArg ColourArg = completeColour (prev, next)

121151 completeArg NoArg = noCompletion (prev, next)

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

123153

src/Idris/Help.hs+10−7

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

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

77 | OptionArg -- ^ The command takes an option

88 | MetaVarArg -- ^ The command takes a metavariable

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

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

1011 | SpecialHeaderArg -- ^ do not use

1112

1213instance Show CmdArg where

13− show ExprArg = "<expr>"

14− show NameArg = "<name>"

15− show FileArg = "<filename>"

16− show ModuleArg = "<module>"

17− show OptionArg = "<option>"

18− show MetaVarArg = "<metavar>"

19− show NoArg = ""

14+ show ExprArg = "<expr>"

15+ show NameArg = "<name>"

16+ show FileArg = "<filename>"

17+ show ModuleArg = "<module>"

18+ show OptionArg = "<option>"

19+ show MetaVarArg = "<metavar>"

20+ show ColourArg = "<option>"

21+ show NoArg = ""

2022 show SpecialHeaderArg = "Arguments"

2123

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

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

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

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

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

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

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

5053 ]

src/Idris/REPL.hs+12−2

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

2020import Idris.IdeSlave

2121import Idris.Chaser

2222import Idris.Imports

23+import Idris.Colours

2324

2425import Paths_idris

2526import Util.System

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

6869repl orig mods

6970 = H.catch

7071 (do let quiet = opt_quiet (idris_options orig)

72+ i <- lift getIState

73+ let colour = idris_colourRepl i

74+ let theme = idris_colourTheme i

7175 let prompt = if quiet

7276 then ""

73− else mkPrompt mods ++ "> "

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

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

7479 x <- getInputLine prompt

7580 case x of

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

7782 return ()

78− Just input -> H.catch

83+ Just input -> H.catch

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

8085 case ms of

8186 Just mods -> repl orig mods

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

541546

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

543548process 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 }

544554

545555

546556classInfo :: ClassInfo -> Idris ()

src/Idris/REPLParser.hs+56

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

11module Idris.REPLParser(parseCmd) where

22

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

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

45

6+import Idris.Colours

57import Idris.Parser

68import Idris.AbsSyntax

79import Core.TT

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

1416import Debug.Trace

1517import Data.List

1618import Data.List.Split(splitOn)

19+import Data.Char(toLower)

1720

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

1922

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

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

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

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

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

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

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

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

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

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

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

7377

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)