@@ -1047,6 +1047,29 @@ prettyImp impl = prettySe 10
1047 | inner > outer = lparen <> doc <> rparen
1047 | inner > outer = lparen <> doc <> rparen
1048 | otherwise = doc
1048 | otherwise = doc
1050+-- | Show Idris name
1051+showName :: Maybe IState -- ^^ the Idris state, for information about names
1052+ -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1053+ -> Bool -- ^^ whether to show implicits
1054+ -> Bool -- ^^ whether to colourise
1055+ -> Name -- ^^ the term to show
1057+showName ist bnd impl colour n = if colour then colourise n else showbasic n
1058+ where name = if impl then show n else showbasic n
1059+ showbasic n@(UN _) = show n
1060+ showbasic (MN _ s) = s
1061+ showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1063+ colourise n = let ctxt' = fmap tt_ctxt ist in
1066+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name
1067+ else colouriseBound name
1068+ | isDConName n ctxt -> colouriseData name
1069+ | isFnName n ctxt -> colouriseFun name
1070+ | isTConName n ctxt -> colouriseType name
1071+ | otherwise -> name
1050-- | Show Idris term
1073-- | Show Idris term
1051showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
1074showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
1052 -> Bool -- ^^ whether to show implicits
1075 -> Bool -- ^^ whether to show implicits
@@ -1056,26 +1079,12 @@ showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
1056showImp ist impl colour tm = se 10 [] tm where
1079showImp ist impl colour tm = se 10 [] tm where
1057 perhapsColourise :: (String -> String) -> String -> String
1080 perhapsColourise :: (String -> String) -> String -> String
1058 perhapsColourise col str = if colour then col str else str
1081 perhapsColourise col str = if colour then col str else str
1060 se :: Int -> [(Name, Bool)] -> PTerm -> String
1083 se :: Int -> [(Name, Bool)] -> PTerm -> String
1061 se p bnd (PQuote r) = "![" ++ show r ++ "]"
1084 se p bnd (PQuote r) = "![" ++ show r ++ "]"
1062 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1085 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1063 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1086 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1064− se p bnd (PRef fc n) = if colour then colourise n else showbasic n
1087+ se p bnd (PRef fc n) = showName ist bnd impl colour n
1065− where name = if impl then show n else showbasic n
1066− showbasic n@(UN _) = show n
1067− showbasic (MN _ s) = s
1068− showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1070− colourise n = let ctxt' = fmap tt_ctxt ist in
1073− Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name
1074− else colouriseBound name
1075− | isDConName n ctxt -> colouriseData name
1076− | isFnName n ctxt -> colouriseFun name
1077− | isTConName n ctxt -> colouriseType name
1078− | otherwise -> name
1079 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1088 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1080 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1089 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1081 ++ se 10 ((n, False):bnd) sc
1090 ++ se 10 ((n, False):bnd) sc