From 549eec8a0622b04eeac3348a588579ca483985a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Aug 2015 18:22:59 -0700
Subject: [PATCH] test(tests/shared/name.c): test exception

---
 src/api/name.cpp        |  2 +-
 src/tests/shared/name.c | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/api/name.cpp b/src/api/name.cpp
index 75c661088..bf298e5aa 100644
--- a/src/api/name.cpp
+++ b/src/api/name.cpp
@@ -57,7 +57,7 @@ lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * ex)
     LEAN_TRY;
     check_nonnull(n);
     if (to_name_ref(n).is_anonymous())
-        throw lean::exception("invalid argument, anonymous names does not have a prefix");
+        throw lean::exception("invalid argument, argument is an anonymous name");
     else if (to_name_ref(n).is_atomic())
         *r = of_name(new name());
     else
diff --git a/src/tests/shared/name.c b/src/tests/shared/name.c
index a184874c3..bfbffccb7 100644
--- a/src/tests/shared/name.c
+++ b/src/tests/shared/name.c
@@ -10,12 +10,13 @@ void check(int v) {
 }
 
 int main() {
-    printf("Started name test\n");
     lean_exception ex;
-    lean_name a, n1, n2, n3, n4;
+    lean_name a, n1, n2, n3, n4, n5;
     char const * s1;
     char const * s2;
+    char const * s3;
     unsigned idx;
+    printf("Started name test\n");
     check(lean_mk_anonymous_name(&a, &ex));
     check(lean_is_anonymous_name(a));
     check(lean_mk_str_name(a, "foo", &n1, &ex));
@@ -33,6 +34,9 @@ int main() {
     check(lean_name_eq(n2, n4));
     check(lean_get_name_idx(n3, &idx, &ex));
     check(idx == 1);
+    check(!lean_get_name_prefix(a, &n5, &ex));
+    s3 = lean_get_exception_message(ex);
+    printf("Lean exception: %s\n", s3);
     lean_del_name(a);
     lean_del_name(n1);
     lean_del_name(n2);
@@ -40,5 +44,7 @@ int main() {
     lean_del_name(n4);
     lean_del_string(s1);
     lean_del_string(s2);
+    lean_del_string(s3);
+    lean_del_exception(ex);
     return 0;
 }