@@ -122,7 +122,8 @@ data IState = IState {
122122 idris_dynamic_libs :: [DynamicLib],
123123 idris_language_extensions :: [LanguageExt],
124124 idris_outputmode :: OutputMode,
125− idris_colourRepl :: Bool
125+ idris_colourRepl :: Bool,
126+ idris_colourTheme :: ColourTheme
126127 }
127128
128129data SizeChange = Smaller | Same | Bigger | Unknown
@@ -180,7 +181,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
180181 emptyContext emptyContext emptyContext emptyContext
181182 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] []
182183 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
183− True
184+ True defaultTheme
184185
185186-- | The monad for the main REPL - reading and processing files and updating
186187-- global state (hence the IO inner monad).
@@ -1050,41 +1051,45 @@ prettyImp impl = prettySe 10
10501051 | otherwise = doc
10511052
10521053-- | 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
10541055 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
10551056 -> Bool -- ^^ whether to show implicits
10561057 -> Bool -- ^^ whether to colourise
10571058 -> Name -- ^^ the term to show
10581059 -> String
1059−showName ist bnd impl colour n = if colour then colourise n else showbasic n
1060+showName ist bnd impl colour n = case ist of
1061+ Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1062+ Nothing -> showbasic n
10601063 where name = if impl then show n else showbasic n
10611064 showbasic n@(UN _) = show n
10621065 showbasic (MN _ s) = s
10631066 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
10641067 showbasic (SN s) = show s
10651068 fst3 (x, _, _) = x
1066− colourise n = let ctxt' = fmap tt_ctxt ist in
1067− case ctxt' of
1068− Nothing -> name
1069− Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name
1070− else colouriseBound name
1071− | isDConName n ctxt -> colouriseData name
1072− | isFnName n ctxt -> colouriseFun name
1073− | isTConName n ctxt -> colouriseType name
1074− -- 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
1076− -- (like error messages). Thus, unknown vars are colourised as implicits.
1077− | otherwise -> colouriseImplicit name
1069+ colourise n t = let ctxt' = fmap tt_ctxt ist in
1070+ case ctxt' of
1071+ Nothing -> name
1072+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1073+ else colouriseBound t name
1074+ | isDConName n ctxt -> colouriseData t name
1075+ | isFnName n ctxt -> colouriseFun t name
1076+ | isTConName n ctxt -> colouriseType t name
1077+ -- The assumption is that if a name is not bound and does not exist in the
1078+ -- global context, then we're somewhere in which implicit info has been lost
1079+ -- (like error messages). Thus, unknown vars are colourised as implicits.
1080+ | otherwise -> colouriseImplicit t name
10781081
10791082-- | 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
10811084 -> Bool -- ^^ whether to show implicits
10821085 -> Bool -- ^^ whether to colourise
10831086 -> PTerm -- ^^ the term to show
10841087 -> String
10851088showImp ist impl colour tm = se 10 [] tm where
1086− perhapsColourise :: (String -> String) -> String -> String
1087− perhapsColourise col str = if colour then col str else str
1089+ perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
1090+ perhapsColourise col str = case ist of
1091+ Just i -> if colour then col (idris_colourTheme i) str else str
1092+ Nothing -> str
10881093
10891094 se :: Int -> [(Name, Bool)] -> PTerm -> String
10901095 se p bnd (PQuote r) = "![" ++ show r ++ "]"