git.iko.soy/Idris-dev
on master help sign in
Merge pull request #476 from david-christiansen/color-repl
db47977Edwin Brady
src/Idris/AbsSyntaxTree.hs+24−19
compare with master
unifiedsplit
@@ -122,7 +122,8 @@ data IState = IState {
122 idris_dynamic_libs :: [DynamicLib],
122 idris_dynamic_libs :: [DynamicLib],
123 idris_language_extensions :: [LanguageExt],
123 idris_language_extensions :: [LanguageExt],
124 idris_outputmode :: OutputMode,
124 idris_outputmode :: OutputMode,
125− idris_colourRepl :: Bool
125+ idris_colourRepl :: Bool,
126+ idris_colourTheme :: ColourTheme
126 }
127 }
127
128
128data SizeChange = Smaller | Same | Bigger | Unknown
129data SizeChange = Smaller | Same | Bigger | Unknown
@@ -180,7 +181,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
180 emptyContext emptyContext emptyContext emptyContext
181 emptyContext emptyContext emptyContext emptyContext
181 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] []
182 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] []
182 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
183 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
183− True
184+ True defaultTheme
184
185
185-- | The monad for the main REPL - reading and processing files and updating
186-- | The monad for the main REPL - reading and processing files and updating
186-- global state (hence the IO inner monad).
187-- global state (hence the IO inner monad).
@@ -1050,41 +1051,45 @@ prettyImp impl = prettySe 10
1050 | otherwise = doc
1051 | otherwise = doc
1051
1052
1052-- | Show Idris name
1053-- | Show Idris name
1053−showName :: Maybe IState -- ^^ the Idris state, for information about names
1054+showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1054 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1055 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1055 -> Bool -- ^^ whether to show implicits
1056 -> Bool -- ^^ whether to show implicits
1056 -> Bool -- ^^ whether to colourise
1057 -> Bool -- ^^ whether to colourise
1057 -> Name -- ^^ the term to show
1058 -> Name -- ^^ the term to show
1058 -> String
1059 -> String
1060+showName ist bnd impl colour n = case ist of
1059−showName ist bnd impl colour n = if colour then colourise n else showbasic n
1061+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1062+ Nothing -> showbasic n
1060 where name = if impl then show n else showbasic n
1063 where name = if impl then show n else showbasic n
1061 showbasic n@(UN _) = show n
1064 showbasic n@(UN _) = show n
1062 showbasic (MN _ s) = s
1065 showbasic (MN _ s) = s
1063 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1066 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1064 showbasic (SN s) = show s
1067 showbasic (SN s) = show s
1065 fst3 (x, _, _) = x
1068 fst3 (x, _, _) = x
1066− colourise n = let ctxt' = fmap tt_ctxt ist in
1069+ colourise n t = let ctxt' = fmap tt_ctxt ist in
1067− case ctxt' of
1070+ case ctxt' of
1068− Nothing -> name
1071+ Nothing -> name
1069− Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name
1072+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1070− else colouriseBound name
1073+ else colouriseBound t name
1071− | isDConName n ctxt -> colouriseData name
1074+ | isDConName n ctxt -> colouriseData t name
1072− | isFnName n ctxt -> colouriseFun name
1075+ | isFnName n ctxt -> colouriseFun t name
1073− | isTConName n ctxt -> colouriseType name
1076+ | isTConName n ctxt -> colouriseType t name
1074− -- The assumption is that if a name is not bound and does not exist in the
1077+ -- The assumption is that if a name is not bound and does not exist in the
1075− -- global context, then we're somewhere in which implicit info has been lost
1078+ -- global context, then we're somewhere in which implicit info has been lost
1076− -- (like error messages). Thus, unknown vars are colourised as implicits.
1079+ -- (like error messages). Thus, unknown vars are colourised as implicits.
1077− | otherwise -> colouriseImplicit name
1080+ | otherwise -> colouriseImplicit t name
1078
1081
1079-- | Show Idris term
1082-- | Show Idris term
1080−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
1083+showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours
1081 -> Bool -- ^^ whether to show implicits
1084 -> Bool -- ^^ whether to show implicits
1082 -> Bool -- ^^ whether to colourise
1085 -> Bool -- ^^ whether to colourise
1083 -> PTerm -- ^^ the term to show
1086 -> PTerm -- ^^ the term to show
1084 -> String
1087 -> String
1085showImp ist impl colour tm = se 10 [] tm where
1088showImp ist impl colour tm = se 10 [] tm where
1086− perhapsColourise :: (String -> String) -> String -> String
1089+ perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
1087− perhapsColourise col str = if colour then col str else str
1090+ perhapsColourise col str = case ist of
1091+ Just i -> if colour then col (idris_colourTheme i) str else str
1092+ Nothing -> str
1088
1093
1089 se :: Int -> [(Name, Bool)] -> PTerm -> String
1094 se :: Int -> [(Name, Bool)] -> PTerm -> String
1090 se p bnd (PQuote r) = "![" ++ show r ++ "]"
1095 se p bnd (PQuote r) = "![" ++ show r ++ "]"
src/Idris/Colours.hs+49−22
@@ -1,32 +1,59 @@
1−module Idris.Colours where
1+module Idris.Colours (
2+ IdrisColour(..),
3+ ColourTheme(..),
4+ defaultTheme,
5+ colouriseKwd, colouriseBound, colouriseImplicit,
6+ colouriseType, colouriseFun, colouriseData) where
2
7
3import System.Console.ANSI
8import System.Console.ANSI
4
9
10+data IdrisColour = IdrisColour { colour :: Color
11+ , vivid :: Bool
12+ , underline :: Bool
13+ , bold :: Bool
14+ }
15+
16+mkColour :: Color -> IdrisColour
17+mkColour c = IdrisColour c True False False
18+
19+data ColourTheme = ColourTheme { keywordColour :: IdrisColour
20+ , boundVarColour :: IdrisColour
21+ , implicitColour :: IdrisColour
22+ , functionColour :: IdrisColour
23+ , typeColour :: IdrisColour
24+ , dataColour :: IdrisColour
25+ }
26+
27+defaultTheme :: ColourTheme
28+defaultTheme = ColourTheme { keywordColour = IdrisColour Black True True True
29+ , boundVarColour = mkColour Magenta
30+ , implicitColour = IdrisColour Magenta True True False
31+ , functionColour = mkColour Green
32+ , typeColour = mkColour Blue
33+ , dataColour = mkColour Red
34+ }
35+
5-- Set the colour of a string using POSIX escape codes
36-- Set the colour of a string using POSIX escape codes
6−colourise :: Color -> ColorIntensity -> String -> String
37+colourise :: IdrisColour -> String -> String
38+colourise (IdrisColour c v u b) str = setSGRCode sgr ++ str ++ setSGRCode [Reset]
7−colourise c i str = let sgr = [SetColor Foreground i c]
39+ where sgr = [SetColor Foreground (if v then Vivid else Dull) c] ++
8− in setSGRCode sgr ++ str ++ setSGRCode [Reset]
40+ (if u then [SetUnderlining SingleUnderline] else []) ++
41+ (if b then [SetConsoleIntensity BoldIntensity] else [])
9
42
10−colouriseKwd :: String -> String
43+colouriseKwd :: ColourTheme -> String -> String
11−colouriseKwd kwd = setSGRCode [SetUnderlining SingleUnderline
44+colouriseKwd t = colourise (keywordColour t)
12− , SetConsoleIntensity BoldIntensity
13− , SetColor Foreground Vivid Black
14− ] ++ kwd ++ setSGRCode [Reset]
15
45
16−colouriseBound :: String -> String
46+colouriseBound :: ColourTheme -> String -> String
17−colouriseBound = colourise Magenta Vivid
47+colouriseBound t = colourise (boundVarColour t)
18
48
19−colouriseImplicit :: String -> String
49+colouriseImplicit :: ColourTheme -> String -> String
20−colouriseImplicit str = let sgr = [ SetColor Foreground Vivid Magenta
50+colouriseImplicit t = colourise (implicitColour t)
21− , SetUnderlining SingleUnderline
22− ]
23− in setSGRCode sgr ++ str ++ setSGRCode [Reset]
24
51
25−colouriseFun :: String -> String
52+colouriseFun :: ColourTheme -> String -> String
26−colouriseFun = colourise Green Vivid
53+colouriseFun t = colourise (functionColour t)
27
54
28−colouriseType :: String -> String
55+colouriseType :: ColourTheme -> String -> String
29−colouriseType = colourise Blue Vivid
56+colouriseType t = colourise (typeColour t)
30
57
31−colouriseData :: String -> String
58+colouriseData :: ColourTheme -> String -> String
32−colouriseData = colourise Red Vivid
59+colouriseData t = colourise (dataColour t)