@@ -804,6 +804,12 @@ colouriseKwd kwd = setSGRCode [SetUnderlining SingleUnderline
804804colouriseBound :: String -> String
805805colouriseBound = colourise Magenta Vivid
806806
807+colouriseImplicit :: String -> String
808+colouriseImplicit str = let sgr = [ SetColor Foreground Vivid Magenta
809+ , SetUnderlining SingleUnderline
810+ ]
811+ in setSGRCode sgr ++ str ++ setSGRCode [Reset]
812+
807813colouriseFun :: String -> String
808814colouriseFun = colourise Green Vivid
809815
@@ -1076,7 +1082,7 @@ showImp ist impl colour tm = se 10 [] tm where
10761082 perhapsColourise :: (String -> String) -> String -> String
10771083 perhapsColourise col str = if colour then col str else str
10781084
1079− se :: Int -> [Name] -> PTerm -> String
1085+ se :: Int -> [(Name, Bool)] -> PTerm -> String
10801086 se p bnd (PQuote r) = "![" ++ show r ++ "]"
10811087 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
10821088 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
@@ -1089,24 +1095,25 @@ showImp ist impl colour tm = se 10 [] tm where
10891095 colourise n = let ctxt' = fmap tt_ctxt ist in
10901096 case ctxt' of
10911097 Nothing -> name
1092− Just ctxt | n `elem` bnd -> colouriseBound name
1098+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name
1099+ else colouriseBound name
10931100 | isDConName n ctxt -> colouriseData name
10941101 | isFnName n ctxt -> colouriseFun name
10951102 | isTConName n ctxt -> colouriseType name
1096− | otherwise -> name
1103+ | otherwise -> name
10971104 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
10981105 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1099− ++ se 10 (n:bnd) sc
1106+ ++ se 10 ((n, False):bnd) sc
11001107 se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
11011108 " = " ++ se 10 bnd v ++
1102− " in " ++ se 10 (n:bnd) sc
1109+ " in " ++ se 10 ((n, False):bnd) sc
11031110 se p bnd (PPi (Exp l s _) n ty sc)
11041111 | n `elem` allNamesIn sc || impl
11051112 = bracket p 2 $
11061113 (if l then "|(" else "(") ++
11071114 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
11081115 ") " ++ st ++
1109− "-> " ++ se 10 (n:bnd) sc
1116+ "-> " ++ se 10 ((n, False):bnd) sc
11101117 | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
11111118 where st = case s of
11121119 Static -> "[static] "
@@ -1114,8 +1121,8 @@ showImp ist impl colour tm = se 10 [] tm where
11141121 se p bnd (PPi (Imp l s _) n ty sc)
11151122 | impl = bracket p 2 $ (if l then "|{" else "{") ++
11161123 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1117− "} " ++ st ++ "-> " ++ se 10 (n:bnd) sc
1118− | otherwise = se 10 bnd sc
1124+ "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
1125+ | otherwise = se 10 ((n, True):bnd) sc
11191126 where st = case s of
11201127 Static -> "[static] "
11211128 _ -> ""
@@ -1124,7 +1131,7 @@ showImp ist impl colour tm = se 10 [] tm where
11241131 se p bnd (PPi (TacImp _ _ s _) n ty sc)
11251132 = bracket p 2 $
11261133 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1127− se 10 (n:bnd) sc
1134+ se 10 ((n, False):bnd) sc
11281135 se p bnd e
11291136 | Just str <- slist p bnd e = str
11301137 | Just num <- snat p e = perhapsColourise colouriseData (show num)