From 9cf93c82992e6d28de8a314854a3c16f1b4854c3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 31 Jul 2014 17:41:39 -0700
Subject: [PATCH] feat(library/error_handling): add helpers classes for
 creating WARNING and INFO annotations for flycheck

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp             |  2 +-
 src/frontends/lean/parser.cpp                 |  4 ++--
 src/library/error_handling/error_handling.cpp |  6 +++---
 src/library/error_handling/error_handling.h   | 16 ++++++++++++++--
 4 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 55553573c..3ba2b1c59 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1033,7 +1033,7 @@ 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);
+            flycheck_error err(out);
             display_error_pos(out, m_pos_provider, mvar);
             out << " unsolved placeholder, " << msg << "\n" << ps << endl;
         }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 16024f1e5..f7c20c61e 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -133,7 +133,7 @@ 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) {
-    flycheck_scope fcheck(regular_stream());
+    flycheck_error err(regular_stream());
     display_error_pos(line, pos);
     regular_stream() << " " << msg << endl;
 }
@@ -169,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(flycheck_scope fcheck(regular_stream()); regular_stream() << ex.what() << endl,
+        CATCH(flycheck_error err(regular_stream()); regular_stream() << ex.what() << endl,
               throw);
     } catch (parser_error & ex) {
         CATCH(display_error(ex.what(), ex.m_pos),
diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp
index e6954a32d..322f6d785 100644
--- a/src/library/error_handling/error_handling.cpp
+++ b/src/library/error_handling/error_handling.cpp
@@ -16,10 +16,10 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 
 namespace lean {
-flycheck_scope::flycheck_scope(io_state_stream const & ios):
+flycheck_scope::flycheck_scope(io_state_stream const & ios, char const * kind):
     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;
+    if (m_use_flycheck) m_ios << "FLYCHECK_BEGIN " << kind << endl;
 }
 flycheck_scope::~flycheck_scope() {
     if (m_use_flycheck) m_ios << "FLYCHECK_END" << endl;
@@ -141,7 +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) {
-    flycheck_scope fcheck(ios);
+    flycheck_error err(ios);
     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)) {
diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling/error_handling.h
index 98c13ae50..a79aee2a7 100644
--- a/src/library/error_handling/error_handling.h
+++ b/src/library/error_handling/error_handling.h
@@ -13,12 +13,24 @@ namespace lean {
 /** \brief Auxiliary object for "inserting" delimiters for flycheck */
 class flycheck_scope {
     io_state_stream const & m_ios;
-    bool m_use_flycheck;
+    bool                    m_use_flycheck;
 public:
-    flycheck_scope(io_state_stream const & ios);
+    flycheck_scope(io_state_stream const & ios, char const * kind);
     ~flycheck_scope();
 };
 
+struct flycheck_error : public flycheck_scope {
+    flycheck_error(io_state_stream const & ios):flycheck_scope(ios, "ERROR") {}
+};
+
+struct flycheck_warning : public flycheck_scope {
+    flycheck_warning(io_state_stream const & ios):flycheck_scope(ios, "WARNING") {}
+};
+
+struct flycheck_info : public flycheck_scope {
+    flycheck_info(io_state_stream const & ios):flycheck_scope(ios, "INFO") {}
+};
+
 /**
    \brief Display position information associated with \c e (IF avaiable).
    If it is not available, it just displays "error:"