From 4d1b7112479a2b31580eaba658d6a69478c58302 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 May 2015 20:09:15 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): better error localization
 when running out of stack space and/or memory in begin-end tactic mode.

---
 src/frontends/lean/elaborator.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 840c83b23..7a04f8943 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1847,6 +1847,15 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
                 } catch (tactic_exception & ex) {
                     display_tactic_exception(ex, ps, ptac);
                     return false;
+                } catch (exception &) {
+                    throw;
+                } catch (throwable & ex) {
+                    auto out = regular(env(), ios());
+                    flycheck_error err(out);
+                    display_error_pos(out, pip(), ptac);
+                    out << ex.what() << "\nproof state:\n";
+                    out << ps.pp(env(), ios()) << "\n";
+                    return false;
                 }
             } else {
                 return false;