feat(library/error_handling): add flycheck_scope helper class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/elaborator.cpp

@@ -1033,8 +1033,9 @@ public:
         if (!m_displayed_errors.contains(mlocal_name(mvar))) {
             m_displayed_errors.insert(mlocal_name(mvar));
             auto out = regular(m_env, m_ios);
+            flycheck_scope fcheck(out);
             display_error_pos(out, m_pos_provider, mvar);
-            out << " unsolved placeholder, " << msg << "\n" << ps << "\n";
+            out << " unsolved placeholder, " << msg << "\n" << ps << endl;
         }
     }
 

src/frontends/lean/parser.cpp

@@ -133,11 +133,9 @@ void parser::display_error_pos(unsigned line, unsigned pos) {
 void parser::display_error_pos(pos_info p) { display_error_pos(p.first, p.second); }
 
 void parser::display_error(char const * msg, unsigned line, unsigned pos) {
-    bool use_flycheck = regular_stream().get_options().get_bool("use_flycheck", false);
+    flycheck_scope fcheck(regular_stream());
-    if (use_flycheck) regular_stream() << "FLYCHECK_BEGIN ERROR" << endl;
     display_error_pos(line, pos);
     regular_stream() << " " << msg << endl;
-    if (use_flycheck) regular_stream() << "FLYCHECK_END" << endl;
 }
 
 void parser::display_error(char const * msg, pos_info p) {
@@ -171,7 +169,7 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
     //     CATCH(display_error(ex),
     //           throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second));
     } catch (parser_exception & ex) {
-        CATCH(regular_stream() << ex.what() << endl,
+        CATCH(flycheck_scope fcheck(regular_stream()); regular_stream() << ex.what() << endl,
               throw);
     } catch (parser_error & ex) {
         CATCH(display_error(ex.what(), ex.m_pos),

src/library/error_handling/error_handling.cpp

@@ -13,8 +13,18 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/unifier.h"
 #include "library/parser_nested_exception.h"
+#include "library/error_handling/error_handling.h"
 
 namespace lean {
+flycheck_scope::flycheck_scope(io_state_stream const & ios):
+    m_ios(ios),
+    m_use_flycheck(m_ios.get_options().get_bool("use_flycheck", false)) {
+    if (m_use_flycheck) m_ios << "FLYCHECK_BEGIN ERROR" << endl;
+}
+flycheck_scope::~flycheck_scope() {
+    if (m_use_flycheck) m_ios << "FLYCHECK_END" << endl;
+}
+
 void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
     ios << strm_name << ":" << line << ":";
     if (pos != static_cast<unsigned>(-1))
@@ -131,8 +141,7 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
 // }
 
 void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex) {
-    bool use_flycheck = ios.get_options().get_bool("use_flycheck", false);
+    flycheck_scope fcheck(ios);
-    if (use_flycheck) ios << "FLYCHECK_BEGIN ERROR" << endl;
     if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
         display_error(ios, p, *k_ex);
     } else if (auto e_ex = dynamic_cast<unifier_exception const *>(&ex)) {
@@ -151,6 +160,5 @@ void display_error(io_state_stream const & ios, pos_info_provider const * p, exc
     } else {
         ios << "error: " << ex.what() << endl;
     }
-    if (use_flycheck) ios << "FLYCHECK_END" << endl;
 }
 }

src/library/error_handling/error_handling.h

@@ -10,6 +10,15 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 
 namespace lean {
+/** \brief Auxiliary object for "inserting" delimiters for flycheck */
+class flycheck_scope {
+    io_state_stream const & m_ios;
+    bool m_use_flycheck;
+public:
+    flycheck_scope(io_state_stream const & ios);
+    ~flycheck_scope();
+};
+
 /**
    \brief Display position information associated with \c e (IF avaiable).
    If it is not available, it just displays "error:"