diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index daa9ac3d32..c611149d29 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1709,8 +1709,8 @@ class parser::imp {
         }
         switch (st) {
         case status::Done:  return *pr;
-        case status::Eof:   throw parser_error("invalid tactic command, unexpected end of file", pos());
-        case status::Abort: throw parser_error("failed to prove theorem, proof has been aborted", pos());
+        case status::Eof:   throw tactic_cmd_error("invalid tactic command, unexpected end of file", pos(), s);
+        case status::Abort: throw tactic_cmd_error("failed to prove theorem, proof has been aborted", pos(), s);
         default: lean_unreachable(); // LCOV_EXCL_LINE
         }
     }
diff --git a/tests/lean/interactive/t10.lean.expected.out b/tests/lean/interactive/t10.lean.expected.out
index fd82763094..06ad68cb00 100644
--- a/tests/lean/interactive/t10.lean.expected.out
+++ b/tests/lean/interactive/t10.lean.expected.out
@@ -15,4 +15,6 @@ no goals
 ## Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A
 ## Error (line: 18, pos: 0) failed to prove theorem, proof has been aborted
+Proof state:
+A : Bool, B : Bool, H : A ∧ B, H1 : A, H2 : B ⊢ B ∧ A
 # echo command after failure
diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out
index 6b29f63b65..a2ad66205d 100644
--- a/tests/lean/interactive/t2.lean.expected.out
+++ b/tests/lean/interactive/t2.lean.expected.out
@@ -11,6 +11,8 @@ H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
 ## Proof state:
 H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
 ## Error (line: 9, pos: 5) failed to prove theorem, proof has been aborted
+Proof state:
+H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
 #   Assumed: a
   Assumed: b
 # Variable a : Bool