@@ -1047,6 +1047,29 @@ prettyImp impl = prettySe 10
10471047 | inner > outer = lparen <> doc <> rparen
10481048 | otherwise = doc
10491049
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
1056+ -> String
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
1062+ fst3 (x, _, _) = x
1063+ colourise n = let ctxt' = fmap tt_ctxt ist in
1064+ case ctxt' of
1065+ Nothing -> name
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
1072+
10501073-- | Show Idris term
10511074showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
10521075 -> Bool -- ^^ whether to show implicits
@@ -1056,26 +1079,12 @@ showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
10561079showImp ist impl colour tm = se 10 [] tm where
10571080 perhapsColourise :: (String -> String) -> String -> String
10581081 perhapsColourise col str = if colour then col str else str
1059−
1082+
10601083 se :: Int -> [(Name, Bool)] -> PTerm -> String
10611084 se p bnd (PQuote r) = "![" ++ show r ++ "]"
10621085 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
10631086 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
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
1069− fst3 (x, _, _) = x
1070− colourise n = let ctxt' = fmap tt_ctxt ist in
1071− case ctxt' of
1072− Nothing -> name
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
1087+ se p bnd (PRef fc n) = showName ist bnd impl colour n
10791088 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
10801089 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
10811090 ++ se 10 ((n, False):bnd) sc