From d50fa26ca24efac4e8937b50fbbb73752a0e3ec8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 27 Jul 2015 18:55:20 -0700
Subject: [PATCH] fix(frontends/lean/parser): caching problem when using "show
 hole" and "show goal" command line options

---
 src/frontends/lean/parser.cpp | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 37241ef3e..d9246d8dc 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -190,11 +190,16 @@ void parser::add_abbrev_index(name const & a, name const & d) {
 }
 
 bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const {
-    if (!m_info_manager)
-        return true; // we are not tracking info
-    for (unsigned i = start_line; i <= end_line; i++)
-        if (m_info_manager->is_invalidated(i))
+    if (m_stop_at) {
+        if (start_line <= m_stop_at_line && m_stop_at_line <= end_line)
             return false;
+    }
+    if (m_info_manager) {
+        // we are tracking info
+        for (unsigned i = start_line; i <= end_line; i++)
+            if (m_info_manager->is_invalidated(i))
+                return false;
+    }
     return true;
 }