@@ -804,6 +804,12 @@ colouriseKwd kwd = setSGRCode [SetUnderlining SingleUnderline
804colouriseBound :: String -> String
804colouriseBound :: String -> String
805colouriseBound = colourise Magenta Vivid
805colouriseBound = colourise Magenta Vivid
807+colouriseImplicit :: String -> String
808+colouriseImplicit str = let sgr = [ SetColor Foreground Vivid Magenta
809+ , SetUnderlining SingleUnderline
811+ in setSGRCode sgr ++ str ++ setSGRCode [Reset]
807colouriseFun :: String -> String
813colouriseFun :: String -> String
808colouriseFun = colourise Green Vivid
814colouriseFun = colourise Green Vivid
@@ -1076,7 +1082,7 @@ showImp ist impl colour tm = se 10 [] tm where
1076 perhapsColourise :: (String -> String) -> String -> String
1082 perhapsColourise :: (String -> String) -> String -> String
1077 perhapsColourise col str = if colour then col str else str
1083 perhapsColourise col str = if colour then col str else str
1079− se :: Int -> [Name] -> PTerm -> String
1085+ se :: Int -> [(Name, Bool)] -> PTerm -> String
1080 se p bnd (PQuote r) = "![" ++ show r ++ "]"
1086 se p bnd (PQuote r) = "![" ++ show r ++ "]"
1081 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1087 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1082 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1088 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
@@ -1089,24 +1095,25 @@ showImp ist impl colour tm = se 10 [] tm where
1089 colourise n = let ctxt' = fmap tt_ctxt ist in
1095 colourise n = let ctxt' = fmap tt_ctxt ist in
1090 case ctxt' of
1096 case ctxt' of
1091 Nothing -> name
1097 Nothing -> name
1098+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name
1092− Just ctxt | n `elem` bnd -> colouriseBound name
1099+ else colouriseBound name
1093 | isDConName n ctxt -> colouriseData name
1100 | isDConName n ctxt -> colouriseData name
1094 | isFnName n ctxt -> colouriseFun name
1101 | isFnName n ctxt -> colouriseFun name
1095 | isTConName n ctxt -> colouriseType name
1102 | isTConName n ctxt -> colouriseType name
1096− | otherwise -> name
1103+ | otherwise -> name
1097 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1104 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1098 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1105 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1099− ++ se 10 (n:bnd) sc
1106+ ++ se 10 ((n, False):bnd) sc
1100 se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1107 se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1101 " = " ++ se 10 bnd v ++
1108 " = " ++ se 10 bnd v ++
1102− " in " ++ se 10 (n:bnd) sc
1109+ " in " ++ se 10 ((n, False):bnd) sc
1103 se p bnd (PPi (Exp l s _) n ty sc)
1110 se p bnd (PPi (Exp l s _) n ty sc)
1104 | n `elem` allNamesIn sc || impl
1111 | n `elem` allNamesIn sc || impl
1105 = bracket p 2 $
1112 = bracket p 2 $
1106 (if l then "|(" else "(") ++
1113 (if l then "|(" else "(") ++
1107 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1114 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1108 ") " ++ st ++
1115 ") " ++ st ++
1109− "-> " ++ se 10 (n:bnd) sc
1116+ "-> " ++ se 10 ((n, False):bnd) sc
1110 | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
1117 | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
1111 where st = case s of
1118 where st = case s of
1112 Static -> "[static] "
1119 Static -> "[static] "
@@ -1114,8 +1121,8 @@ showImp ist impl colour tm = se 10 [] tm where
1114 se p bnd (PPi (Imp l s _) n ty sc)
1121 se p bnd (PPi (Imp l s _) n ty sc)
1115 | impl = bracket p 2 $ (if l then "|{" else "{") ++
1122 | impl = bracket p 2 $ (if l then "|{" else "{") ++
1116 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1123 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1117− "} " ++ st ++ "-> " ++ se 10 (n:bnd) sc
1124+ "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
1118− | otherwise = se 10 bnd sc
1125+ | otherwise = se 10 ((n, True):bnd) sc
1119 where st = case s of
1126 where st = case s of
1120 Static -> "[static] "
1127 Static -> "[static] "
@@ -1124,7 +1131,7 @@ showImp ist impl colour tm = se 10 [] tm where
1124 se p bnd (PPi (TacImp _ _ s _) n ty sc)
1131 se p bnd (PPi (TacImp _ _ s _) n ty sc)
1125 = bracket p 2 $
1132 = bracket p 2 $
1126 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1133 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1127− se 10 (n:bnd) sc
1134+ se 10 ((n, False):bnd) sc
1128 se p bnd e
1135 se p bnd e
1129 | Just str <- slist p bnd e = str
1136 | Just str <- slist p bnd e = str
1130 | Just num <- snat p e = perhapsColourise colouriseData (show num)
1137 | Just num <- snat p e = perhapsColourise colouriseData (show num)