fix(frontends/lean): fixes #1292

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");

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();

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) {

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);

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

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