refactor(library): move flycheck "helper" classes to separate module

src/frontends/lean/elaborator.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/let.h"
 #include "library/sorry.h"
+#include "library/flycheck.h"
 #include "library/deep_copy.h"
 #include "library/metavar_closure.h"
 #include "library/typed_expr.h"

src/frontends/lean/parser.cpp

@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/string.h"
 #include "library/sorry.h"
+#include "library/flycheck.h"
 #include "library/error_handling/error_handling.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/tokens.h"

src/library/CMakeLists.txt

@@ -10,6 +10,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   definition_cache.cpp declaration_index.cpp
   print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
   protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp
-  fingerprint.cpp)
+  fingerprint.cpp flycheck.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/error_handling/error_handling.cpp

@@ -14,26 +14,9 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/parser_nested_exception.h"
 #include "library/error_handling/error_handling.h"
+#include "library/flycheck.h"
 
 namespace lean {
-flycheck_scope::flycheck_scope(io_state_stream const & ios, char const * kind):
-    m_ios(ios),
-    m_flycheck(m_ios.get_options().get_bool("flycheck", false)) {
-    if (m_flycheck) m_ios << "FLYCHECK_BEGIN " << kind << endl;
-}
-flycheck_scope::~flycheck_scope() {
-    if (m_flycheck) m_ios << "FLYCHECK_END" << endl;
-}
-
-flyinfo_scope::flyinfo_scope(io_state_stream const & ios):
-    m_ios(ios),
-    m_flyinfo(m_ios.get_options().get_bool("flyinfo", false)) {
-    if (m_flyinfo) m_ios << "FLYCHECK_BEGIN INFO" << endl;
-}
-flyinfo_scope::~flyinfo_scope() {
-    if (m_flyinfo) m_ios << "FLYCHECK_END" << endl;
-}
-
 void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
     ios << strm_name << ":";
     if (ios.get_options().get_bool("flycheck", false)) {

src/library/error_handling/error_handling.h

@@ -10,31 +10,6 @@ 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_flycheck;
-public:
-    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") {}
-};
-
-class flyinfo_scope {
-    io_state_stream const & m_ios;
-    bool                    m_flyinfo;
-public:
-    flyinfo_scope(io_state_stream const & ios);
-    ~flyinfo_scope();
-};
-
 /**
    \brief Display position information associated with \c e (IF avaiable).
    If it is not available, it just displays "error:"

src/library/flycheck.cpp

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/flycheck.h"
+
+namespace lean {
+flycheck_scope::flycheck_scope(io_state_stream const & ios, char const * kind):
+    m_ios(ios),
+    m_flycheck(m_ios.get_options().get_bool("flycheck", false)) {
+    if (m_flycheck) m_ios << "FLYCHECK_BEGIN " << kind << endl;
+}
+flycheck_scope::~flycheck_scope() {
+    if (m_flycheck) m_ios << "FLYCHECK_END" << endl;
+}
+
+flyinfo_scope::flyinfo_scope(io_state_stream const & ios):
+    m_ios(ios),
+    m_flyinfo(m_ios.get_options().get_bool("flyinfo", false)) {
+    if (m_flyinfo) m_ios << "FLYCHECK_BEGIN INFO" << endl;
+}
+flyinfo_scope::~flyinfo_scope() {
+    if (m_flyinfo) m_ios << "FLYCHECK_END" << endl;
+}
+}

src/library/flycheck.h

@@ -0,0 +1,35 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#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_flycheck;
+public:
+    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") {}
+};
+
+class flyinfo_scope {
+    io_state_stream const & m_ios;
+    bool                    m_flyinfo;
+public:
+    flyinfo_scope(io_state_stream const & ios);
+    ~flyinfo_scope();
+};
+}