Skip to content
Browse files

Error message tinker

  • Loading branch information...
1 parent ae4be75 commit 8baaa424e36a96bc3697deb85e6b89a8d3d9636f Edwin Brady committed
Showing with 13 additions and 6 deletions.
  1. +4 −0 CHANGELOG
  2. +2 −2 idris.cabal
  3. +6 −3 src/Idris/Delaborate.hs
  4. +1 −1 tutorial/examples/Makefile
View
4 CHANGELOG
@@ -1,3 +1,7 @@
+New in 0.9.1:
+
+* dsl notation
+
0.1.x to 0.9.0:
Complete rewrite. User visible changes:
View
4 idris.cabal
@@ -1,5 +1,5 @@
Name: idris
-Version: 0.9.0
+Version: 0.9.1
License: BSD3
License-file: LICENSE
Author: Edwin Brady
@@ -8,7 +8,7 @@ Homepage: http://www.idris-lang.org/
Stability: Beta
Category: Compilers/Interpreters, Dependent Types
-Synopsis: Dependently Typed Functional Programming Language
+Synopsis: Functional Programming Language with Dependent Types
Description: Idris is a general purpose language with full dependent types.
It is compiled, with eager evaluation.
Dependent types allow types to be predicated on values,
View
9 src/Idris/Delaborate.hs
@@ -64,9 +64,12 @@ delab' ist tm fullname = de [] tm
pshow :: IState -> Err -> String
pshow i (Msg s) = s
-pshow i (CantUnify x y e s) = "Can't unify " ++ show (delab i x)
- ++ " with " ++ show (delab i y)
--- ++ "\n\t(" ++ pshow i e ++ ")"
+pshow i (CantUnify x y e s)
+ = "Can't unify " ++ show (delab i x)
+ ++ " with " ++ show (delab i y) ++
+ case e of
+ Msg "" -> ""
+ _ -> "\n\nSpecifically:\n\t " ++ pshow i e
pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
" when unifying " ++ show (delab i x) ++ " and " ++
show (delab i y)
View
2 tutorial/examples/Makefile
@@ -1,5 +1,5 @@
check: .PHONY
- rm *.ibc
+ rm -f *.ibc
for x in *.idr ; do \
echo "Checking $$x"; \
idris --check $$x; \

0 comments on commit 8baaa42

Please sign in to comment.
Something went wrong with that request. Please try again.