git.iko.soy/Idris-dev
on master help sign in
Colour theme in Idris REPL state
7c45129David Christiansen
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+18−13
@@ -1,4 +1,9 @@
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
@@ -35,20 +40,20 @@ colourise (IdrisColour c v u b) str = setSGRCode sgr ++ str ++ setSGRCode [Reset
35 (if u then [SetUnderlining SingleUnderline] else []) ++
40 (if u then [SetUnderlining SingleUnderline] else []) ++
36 (if b then [SetConsoleIntensity BoldIntensity] else [])
41 (if b then [SetConsoleIntensity BoldIntensity] else [])
37
42
38−colouriseKwd :: String -> String
43+colouriseKwd :: ColourTheme -> String -> String
39−colouriseKwd = colourise (keywordColour defaultTheme)
44+colouriseKwd t = colourise (keywordColour t)
40
45
41−colouriseBound :: String -> String
46+colouriseBound :: ColourTheme -> String -> String
42−colouriseBound = colourise (boundVarColour defaultTheme)
47+colouriseBound t = colourise (boundVarColour t)
43
48
44−colouriseImplicit :: String -> String
49+colouriseImplicit :: ColourTheme -> String -> String
45−colouriseImplicit = colourise (implicitColour defaultTheme)
50+colouriseImplicit t = colourise (implicitColour t)
46
51
47−colouriseFun :: String -> String
52+colouriseFun :: ColourTheme -> String -> String
48−colouriseFun = colourise (functionColour defaultTheme)
53+colouriseFun t = colourise (functionColour t)
49
54
50−colouriseType :: String -> String
55+colouriseType :: ColourTheme -> String -> String
51−colouriseType = colourise (typeColour defaultTheme)
56+colouriseType t = colourise (typeColour t)
52
57
53−colouriseData :: String -> String
58+colouriseData :: ColourTheme -> String -> String
54−colouriseData = colourise (dataColour defaultTheme)
59+colouriseData t = colourise (dataColour t)