From 384ccf2b6cd45c184f6eac2384268e8c0b31c9a8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jul 2015 17:34:42 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): change behavior of "show
 goal" for incomplete "by tactic"

If "by tactic" did not completely solved the goal, then we show the
final state when the user presses "C-c C-g"
---
 src/frontends/lean/elaborator.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 6325405c9..af7f27b93 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1784,27 +1784,30 @@ bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state
     lean_assert(length(ps.get_goals()) == 1);
     // make sure ps is a really a proof state for mvar.
     lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar));
-    show_goal(ps, pre_tac, pre_tac, pre_tac);
     try {
         proof_state_seq seq = tac(env(), ios(), ps);
         auto r = seq.pull();
         if (!r) {
+            show_goal(ps, pre_tac, pre_tac, pre_tac);
             // tactic failed to produce any result
             if (show_failure)
                 display_unsolved_proof_state(mvar, ps, "tactic failed");
             return false;
         } else if (!empty(r->first.get_goals())) {
             // tactic contains unsolved subgoals
+            show_goal(r->first, pre_tac, pre_tac, pre_tac);
             if (show_failure)
                 display_unsolved_subgoals(mvar, r->first);
             return false;
         } else {
+            show_goal(ps, pre_tac, pre_tac, pre_tac);
             subst = r->first.get_subst();
             expr v = subst.instantiate(mvar);
             subst.assign(mlocal_name(mvar), v);
             return true;
         }
     } catch (tactic_exception & ex) {
+        show_goal(ps, pre_tac, pre_tac, pre_tac);
         if (show_failure)
             display_tactic_exception(ex, ps, pre_tac);
         return false;