From fb7351491334ff1407f3f1d43ce1cc6f43f1e5b3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Jan 2014 15:04:28 -0800
Subject: [PATCH] fix(frontends/lean/parser): parser aborted if the scanner
 throws an exception in the first call to scan(); position information was
 being shown twice for scanner exceptions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser_error.cpp | 62 +++++++++--------------------
 src/frontends/lean/parser_imp.cpp   | 22 +++++-----
 src/frontends/lean/parser_imp.h     |  1 +
 3 files changed, 32 insertions(+), 53 deletions(-)

diff --git a/src/frontends/lean/parser_error.cpp b/src/frontends/lean/parser_error.cpp
index b031f066a..a848a85b6 100644
--- a/src/frontends/lean/parser_error.cpp
+++ b/src/frontends/lean/parser_error.cpp
@@ -97,6 +97,14 @@ void parser_imp::display_error(tactic_cmd_error const & ex) {
     display_proof_state(ex.m_state);
 }
 
+#define CATCH_CORE(ShowError, ThrowError)       \
+m_found_errors = true;                          \
+if (m_show_errors) { ShowError ; }              \
+sync();                                         \
+if (m_use_exceptions) { ThrowError ; }
+
+#define CATCH(ShowError) CATCH_CORE(ShowError, throw;)
+
 /**
    \brief Execute the given function \c f, and handle exceptions occurring
    when executing \c f.
@@ -106,63 +114,29 @@ void parser_imp::protected_call(std::function<void()> && f, std::function<void()
     try {
         f();
     } catch (tactic_cmd_error & ex) {
-        m_found_errors = true;
-        if (m_show_errors)
-            display_error(ex);
-        sync();
-        if (m_use_exceptions)
-            throw;
+        CATCH(display_error(ex));
+    } catch (parser_exception & ex) {
+        CATCH(regular(m_io_state) << "Error " << ex.what() << endl;);
     } catch (parser_error & ex) {
-        m_found_errors = true;
-        if (m_show_errors)
-            display_error(ex.what(), ex.m_pos.first, ex.m_pos.second);
-        sync();
-        if (m_use_exceptions) {
-            throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
-        }
+        CATCH_CORE(display_error(ex.what(), ex.m_pos.first, ex.m_pos.second), throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second));
     } catch (kernel_exception & ex) {
-        m_found_errors = true;
-        if (m_show_errors)
-            display_error(ex);
-        sync();
-        if (m_use_exceptions)
-            throw;
+        CATCH(display_error(ex));
     } catch (elaborator_exception & ex) {
-        m_found_errors = true;
-        if (m_show_errors)
-            display_error(ex);
-        sync();
-        if (m_use_exceptions)
-            throw;
+        CATCH(display_error(ex));
     } catch (metavar_not_synthesized_exception & ex) {
-        m_found_errors = true;
-        if (m_show_errors)
-            display_error(ex);
-        sync();
-        if (m_use_exceptions)
-            throw;
+        CATCH(display_error(ex));
     } catch (script_exception & ex) {
-        m_found_errors = true;
         reset_interrupt();
-        if (m_show_errors)
-            display_error(ex);
-        sync();
-        if (m_use_exceptions)
-            throw;
+        CATCH(display_error(ex));
     } catch (interrupted & ex) {
+        reset_interrupt();
         if (m_verbose)
             regular(m_io_state) << "!!!Interrupted!!!" << endl;
-        reset_interrupt();
         sync();
         if (m_use_exceptions)
             throw;
     } catch (exception & ex) {
-        m_found_errors = true;
-        if (m_show_errors)
-            display_error(ex.what());
-        sync();
-        if (m_use_exceptions)
-            throw;
+        CATCH(display_error(ex.what()););
     }
 }
 }
diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp
index d6b53ac32..c3a11499b 100644
--- a/src/frontends/lean/parser_imp.cpp
+++ b/src/frontends/lean/parser_imp.cpp
@@ -132,6 +132,15 @@ void parser_imp::parse_script(bool as_expr) {
 
 void parser_imp::parse_script_expr() { return parse_script(true); }
 
+void parser_imp::sync_command() {
+    // Keep consuming tokens until we find a Command or End-of-file
+    show_prompt();
+    while (curr() != scanner::token::CommandId && curr() != scanner::token::Eof && curr() != scanner::token::Period)
+        next();
+    if (curr_is_period())
+        next();
+}
+
 parser_imp::parser_imp(environment const & env, io_state const & st, std::istream & in,
                        script_state * S, bool use_exceptions, bool interactive):
     m_env(env),
@@ -162,7 +171,8 @@ parser_imp::parser_imp(environment const & env, io_state const & st, std::istrea
         m_tactic_macros = nullptr;
         m_cmd_macros    = nullptr;
     }
-    scan();
+    protected_call([&]() { scan(); },
+                   [&]() { sync_command(); });
 }
 
 parser_imp::~parser_imp() {}
@@ -199,14 +209,8 @@ bool parser_imp::parse_commands() {
                 default:
                     throw parser_error("Command expected", pos());
                 }
-            }, [&]() {
-                // Keep consuming tokens until we find a Command or End-of-file
-                show_prompt();
-                while (curr() != scanner::token::CommandId && curr() != scanner::token::Eof && curr() != scanner::token::Period)
-                    next();
-                if (curr_is_period())
-                    next();
-            });
+            },
+            [&]() { sync_command(); });
     }
     return !m_found_errors;
 }
diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h
index f2be60a32..2a98c1624 100644
--- a/src/frontends/lean/parser_imp.h
+++ b/src/frontends/lean/parser_imp.h
@@ -421,6 +421,7 @@ private:
     void parse_end();
     void parse_using();
     bool parse_command();
+    void sync_command();
     /*@}*/
 
 public: