on master help sign in
Merge pull request #471 from david-christiansen/color-repl

Colourise some error messages

commit675cfac4194a270fa3e534599ae0eb3da5ebed0d authorEdwin Brady <edwin.brady@gmail.com> dateWed 4 Sep 2013, 11:48 (13 years ago) parent96d05c0ddc137e
5 files changed+26−18
src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Delaborate.hs+18−13 test/reg010/run+1−1 test/test020/run+1−1 test/test030/run+2−2
src/Idris/AbsSyntaxTree.hs+4−1
@@ -1068,7 +1068,10 @@ showName ist bnd impl colour n = if colour then colourise n else showbasic n
10681068 | isDConName n ctxt -> colouriseData name
10691069 | isFnName n ctxt -> colouriseFun name
10701070 | isTConName n ctxt -> colouriseType name
1071− | otherwise -> name
1071+ -- The assumption is that if a name is not bound and does not exist in the
1072+ -- global context, then we're somewhere in which implicit info has been lost
1073+ -- (like error messages). Thus, unknown vars are colourised as implicits.
1074+ | otherwise -> colouriseImplicit name
10721075
10731076-- | Show Idris term
10741077showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers
src/Idris/Delaborate.hs+18−13
@@ -98,35 +98,40 @@ pshow i (Msg s) = s
9898pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
9999 "\nThis is probably a bug, or a missing error message.\n" ++
100100 "Please consider reporting at " ++ bugaddr
101−pshow i (CantUnify _ x y e sc s)
101+pshow i (CantUnify _ x y e sc s)
102102 = let imps = opt_showimp (idris_options i) in
103− "Can't unify " ++ showImp Nothing imps False (delab i x)
104− ++ " with " ++ showImp Nothing imps False (delab i y) ++
103+ let colour = idris_colourRepl i in
104+ "Can't unify " ++ showImp (Just i) imps colour (delab i x)
105+ ++ " with " ++ showImp (Just i) imps colour (delab i y) ++
105106-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
106107 case e of
107108 Msg "" -> ""
108− _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
109+ _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
109110 if (opt_errContext (idris_options i)) then showSc i sc else ""
110−pshow i (CantConvert x y env)
111+pshow i (CantConvert x y env)
111112 = let imps = opt_showimp (idris_options i) in
112− "Can't convert " ++ showImp Nothing imps False (delab i x) ++ " with "
113− ++ showImp Nothing imps False (delab i y) ++
113+ let colour = idris_colourRepl i in
114+ "Can't convert " ++ showImp (Just i) imps colour (delab i x) ++ " with "
115+ ++ showImp (Just i) imps colour (delab i y) ++
114116 if (opt_errContext (idris_options i)) then showSc i env else ""
115−pshow i (UnifyScope n out tm env)
117+pshow i (UnifyScope n out tm env)
116118 = let imps = opt_showimp (idris_options i) in
117− "Can't unify " ++ show n ++ " with "
118− ++ showImp Nothing imps False (delab i tm) ++ " as " ++ show out ++
119+ let colour = idris_colourRepl i in
120+ "Can't unify " ++ show n ++ " with "
121+ ++ showImp (Just i) imps colour (delab i tm) ++ " as " ++ show out ++
119122 " is not in scope" ++
120123 if (opt_errContext (idris_options i)) then showSc i env else ""
121124pshow i (CantInferType t)
122125 = "Can't infer type for " ++ t
123126pshow i (NonFunctionType f ty)
124127 = let imps = opt_showimp (idris_options i) in
125− showImp Nothing imps False (delab i f) ++ " does not have a function type ("
126− ++ showImp Nothing imps False (delab i ty) ++ ")"
128+ let colour = idris_colourRepl i in
129+ showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
130+ ++ showImp (Just i) imps colour (delab i ty) ++ ")"
127131pshow i (CantIntroduce ty)
128132 = let imps = opt_showimp (idris_options i) in
129− "Can't use lambda here: type is " ++ showImp Nothing imps False (delab i ty)
133+ let colour = idris_colourRepl i in
134+ "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
130135pshow i (InfiniteUnify x tm env)
131136 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
132137 " would lead to infinite value" ++
test/reg010/run+1−1
@@ -1,2 +1,2 @@
11#!/bin/bash
2−idris $@ reg010.idr --check
2+idris $@ reg010.idr --check --nocolour
test/test020/run+1−1
@@ -1,5 +1,5 @@
11#!/bin/bash
22idris $@ test020.idr -o test020
3−idris $@ test020a.idr --check
3+idris $@ test020a.idr --check --nocolor
44./test020
55rm -f test020 *.ibc
test/test030/run+2−2
@@ -1,4 +1,4 @@
11#!/bin/bash
2−idris $@ test030.idr --check
3−idris $@ test030a.idr --check
2+idris $@ test030.idr --check --nocolour
3+idris $@ test030a.idr --check --nocolour
44rm -f *.ibc