From f452cabc34a5bf14e0b32239b381594af79d2c18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Sep 2015 18:00:23 -0700
Subject: [PATCH] feat(api/exception): add lean_exception_get_detailed_message

---
 src/api/exception.cpp    | 21 +++++++++++++++++++++
 src/api/lean_exception.h |  7 +++++++
 src/tests/shared/env.c   | 14 ++++++++++----
 3 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/src/api/exception.cpp b/src/api/exception.cpp
index e75aa464b..7d0f11f0b 100644
--- a/src/api/exception.cpp
+++ b/src/api/exception.cpp
@@ -6,9 +6,12 @@ Author: Leonardo de Moura
 */
 #include "kernel/kernel_exception.h"
 #include "library/unifier.h"
+#include "library/print.h"
 #include "library/tactic/tactic.h"
+#include "library/error_handling/error_handling.h"
 #include "api/exception.h"
 #include "api/string.h"
+using namespace lean; // NOLINT
 
 namespace lean {
 memout_exception * get_memout_exception() {
@@ -39,6 +42,24 @@ char const * lean_exception_get_message(lean_exception e) {
     }
 }
 
+char const * lean_exception_get_detailed_message(lean_exception e) {
+    if (!e)
+        return 0;
+    try {
+        formatter_factory fmtf = mk_print_formatter_factory();
+        std::shared_ptr<output_channel> out(new string_output_channel());
+        io_state ios(fmtf);
+        ios.set_regular_channel(out);
+        ios.set_diagnostic_channel(out);
+        environment env;
+        io_state_stream ioss(env, ios);
+        display_error(ioss, nullptr, *lean::to_exception(e));
+        return mk_string(static_cast<string_output_channel const *>(out.get())->str());
+    } catch (...) {
+        return 0;
+    }
+}
+
 lean_exception_kind lean_exception_get_kind(lean_exception e) {
     lean::throwable * ex = lean::to_exception(e);
     if (!ex)
diff --git a/src/api/lean_exception.h b/src/api/lean_exception.h
index c0ef01d0e..e00b08816 100644
--- a/src/api/lean_exception.h
+++ b/src/api/lean_exception.h
@@ -28,6 +28,13 @@ void lean_exception_del(lean_exception e);
 */
 char const * lean_exception_get_message(lean_exception e);
 
+/** \brief Return basic string/message describing the exception.
+    \remark The string must be deallocated using #lean_string_del.
+    This function is similar to #lean_exception_get_message, but produces
+    more information if available.
+*/
+char const * lean_exception_get_detailed_message(lean_exception e);
+
 typedef enum {
     LEAN_NULL_EXCEPTION,    // null (aka there is no exception)
     LEAN_SYSTEM_EXCEPTION,  // exception generated by the C++ runtime
diff --git a/src/tests/shared/env.c b/src/tests/shared/env.c
index 7728f3788..79918a551 100644
--- a/src/tests/shared/env.c
+++ b/src/tests/shared/env.c
@@ -524,11 +524,17 @@ void test_parser_error() {
                                &new_env, &new_ios, &ex));
     {
         lean_exception ex2 = 0;
-        char const * s;
+        char const * s1 = lean_exception_get_message(ex);
+        char const * s2 = lean_exception_get_detailed_message(ex);
+        char const * s3;
         printf("\nexception kind: %d\n", lean_exception_get_kind(ex));
-        check(lean_exception_to_pp_string(env, ios, ex, &s, &ex2));
-        printf("exception\n%s", s);
-        lean_string_del(s);
+        printf("exception message: %s\n", s1);
+        printf("exception detailed message: %s\n", s2);
+        check(lean_exception_to_pp_string(env, ios, ex, &s3, &ex2));
+        printf("exception: %s\n", s3);
+        lean_string_del(s1);
+        lean_string_del(s2);
+        lean_string_del(s3);
     }
     lean_exception_del(ex);
     lean_env_del(env);