From 5cb06ea912aa08acfb0021849b0282ae5eae16f5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 27 Dec 2016 12:24:29 +0100
Subject: [PATCH] perf(frontends/lean/parser): break at break_at_pos even if
 not on an interesting token

---
 src/frontends/lean/parser.cpp | 6 ++++--
 src/frontends/lean/parser.h   | 6 ++++--
 src/shell/server.cpp          | 4 ++--
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index af52cd789c..e0ccee3798 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -203,7 +203,9 @@ bool parser::check_break_at_pos(pos_info const & p, name const & tk) {
 
 void parser::scan() {
     if (curr_is_identifier() && check_break_at_pos(pos(), get_name_val()))
-        throw break_at_pos_exception(pos(), get_name_val());
+        throw info_at_pos_exception(pos(), get_name_val());
+    if (m_break_at_pos && *m_break_at_pos < pos())
+        throw break_at_pos_exception();
     m_curr = m_scanner.scan(m_env);
 }
 
@@ -1245,7 +1247,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
     auto check_break = [&]() {
         if (check_break_at_pos(pos(), get_token_info().value())) {
             // info is stored at position of first notation token
-            throw break_at_pos_exception(p, first_token);
+            throw info_at_pos_exception(p, first_token);
         }
     };
     buffer<expr>                     args;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 4ae51e9c43..f213bd3412 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -77,12 +77,14 @@ struct snapshot {
 
 typedef std::vector<std::shared_ptr<snapshot const>> snapshot_vector;
 
-class break_at_pos_exception : public std::exception {
+class break_at_pos_exception : public std::exception {};
+
+class info_at_pos_exception : public break_at_pos_exception {
 public:
     pos_info    m_token_pos;
     name        m_token;
 
-    break_at_pos_exception(pos_info const & token_pos, name const & token):
+    info_at_pos_exception(pos_info const & token_pos, name const & token):
             m_token_pos(token_pos), m_token(token) {}
 };
 
diff --git a/src/shell/server.cpp b/src/shell/server.cpp
index b22efd6aa8..9d1c246f25 100644
--- a/src/shell/server.cpp
+++ b/src/shell/server.cpp
@@ -391,7 +391,7 @@ public:
                              use_exceptions, std::make_shared<snapshot>(s), nullptr);
                     p.set_break_at_pos(pos);
                     p();
-                } catch (break_at_pos_exception & e) {
+                } catch (info_at_pos_exception & e) {
                     lean_assert(e.m_token_pos.first == pos.first);
 
                     auto opts = m_server->m_ios.get_options();
@@ -411,7 +411,7 @@ public:
                     }
 
                     j["record"] = record;
-                }
+                } catch (break_at_pos_exception & e) {}
             }
 
             m_server->send_msg(cmd_res(m_seq_num, j));