From 7a150b41b9d3b9d6dababe9bea675e100b93376f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Jan 2017 15:53:37 -0800
Subject: [PATCH] fix(frontends/lean): fixes #1292

---
 src/frontends/lean/match_expr.cpp      | 2 +-
 src/frontends/lean/tactic_notation.cpp | 2 +-
 src/frontends/lean/util.cpp            | 7 ++++---
 src/frontends/lean/util.h              | 4 ++--
 tests/lean/1292.lean                   | 8 ++++++++
 tests/lean/1292.lean.expected.out      | 2 ++
 6 files changed, 18 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/1292.lean
 create mode 100644 tests/lean/1292.lean.expected.out

diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp
index ba68d34726..cfa1996a17 100644
--- a/src/frontends/lean/match_expr.cpp
+++ b/src/frontends/lean/match_expr.cpp
@@ -78,7 +78,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
             p.next();
         }
     } catch (exception & ex) {
-        consume_until_end(p);
+        consume_until_end_or_command(p);
         ex.rethrow();
     }
     p.check_token_next(get_end_tk(), "invalid 'match' expression, 'end' expected");
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index dcc39322cf..fe65767c4f 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -430,7 +430,7 @@ static expr parse_begin_end_block(parser & p, pos_info const & start_pos, name c
         }
     } catch (exception & ex) {
         if (end_token == get_end_tk())
-            consume_until_end(p);
+            consume_until_end_or_command(p);
         throw;
     }
     auto end_pos = p.pos();
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 9e20ab57f1..7f1ffe1628 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -31,13 +31,14 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/decl_util.h" // TODO(Leo): remove
 namespace lean {
-void consume_until_end(parser & p) {
-    while (!p.curr_is_token(get_end_tk())) {
+void consume_until_end_or_command(parser & p) {
+    while (!p.curr_is_command() && !p.curr_is_eof() && !p.curr_is_token(get_period_tk())) {
         if (p.curr() == scanner::token_kind::Eof)
             return;
         p.next();
     }
-    p.next();
+    if (p.curr_is_token(get_end_tk()))
+        p.next();
 }
 
 void check_command_period_or_eof(parser const & p) {
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 3ae11cf66d..eb9738b272 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -15,8 +15,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 class parser;
-/** \brief Consume tokes until 'end' token is consumed */
-void consume_until_end(parser & p);
+/** \brief Consume tokens until 'end' token is consumed or a command/eof is found */
+void consume_until_end_or_command(parser & p);
 
 /** \brief Throw and error if the current token is not a command, nor a '.', nor an end-of-file. */
 void check_command_period_or_eof(parser const & p);
diff --git a/tests/lean/1292.lean b/tests/lean/1292.lean
new file mode 100644
index 0000000000..07579d5027
--- /dev/null
+++ b/tests/lean/1292.lean
@@ -0,0 +1,8 @@
+def fn (n : nat) : nat :=
+match n with
+
+exit
+
+theorem thm : true := begin end
+
+example : has_add nat := sorry
diff --git a/tests/lean/1292.lean.expected.out b/tests/lean/1292.lean.expected.out
new file mode 100644
index 0000000000..5fca1e3ef4
--- /dev/null
+++ b/tests/lean/1292.lean.expected.out
@@ -0,0 +1,2 @@
+1292.lean:4:0: error: invalid expression, unexpected token
+1292.lean:4:0: warning: using 'exit' to interrupt Lean