From 14a406d4d71a94dd254dbd51d7b5a92c9cd86261 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Thu, 31 Jul 2014 11:18:51 -0700
Subject: [PATCH] feat: add "--flycheck" option to print out error msgs for
 flycheck

---
 src/frontends/lean/parser.cpp                 |  3 +++
 src/library/error_handling/error_handling.cpp |  3 +++
 src/shell/lean.cpp                            | 12 ++++++++++--
 3 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index d0bc988e9..250327e66 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -133,8 +133,11 @@ 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);
+    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) {
diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp
index df19257b0..dbe834698 100644
--- a/src/library/error_handling/error_handling.cpp
+++ b/src/library/error_handling/error_handling.cpp
@@ -131,6 +131,8 @@ 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);
+    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)) {
@@ -149,5 +151,6 @@ 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;
 }
 }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index d78399d31..592b827f0 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -75,6 +75,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --hott            use Homotopy Type Theory kernel and libraries\n";
     std::cout << "  --threads=num -j  number of threads used to process lean files\n";
     std::cout << "  --deps            just print dependencies of a Lean input\n";
+    std::cout << "  --flycheck        print structured error message for flycheck\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -109,6 +110,7 @@ static struct option g_long_options[] = {
     {"hott",        no_argument,       0, 'H'},
     {"threads",     required_argument, 0, 'j'},
     {"deps",        no_argument,       0, 'D'},
+    {"flycheck",    no_argument,       0, 'F'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",      required_argument, 0, 's'},
 #endif
@@ -116,9 +118,9 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "DHiqlupgvhj:012c:012s:012t:012o:";
+static char const * g_opt_str = "FDHiqlupgvhj:012c:012s:012t:012o:";
 #else
-static char const * g_opt_str = "DHiqlupgvhj:012c:012t:012o:";
+static char const * g_opt_str = "FDHiqlupgvhj:012c:012t:012o:";
 #endif
 
 enum class lean_mode { Standard, HoTT };
@@ -131,6 +133,7 @@ int main(int argc, char ** argv) {
     bool quiet           = false;
     bool interactive     = false;
     bool only_deps       = false;
+    bool use_flycheck    = false;
     lean_mode mode       = lean_mode::Standard;
     unsigned num_threads = 1;
     std::string output;
@@ -187,6 +190,9 @@ int main(int argc, char ** argv) {
         case 'D':
             only_deps = true;
             break;
+        case 'F':
+            use_flycheck = true;
+            break;
         default:
             std::cerr << "Unknown command line option\n";
             display_help(std::cerr);
@@ -198,6 +204,8 @@ int main(int argc, char ** argv) {
     io_state ios(lean::mk_pretty_formatter_factory());
     if (quiet)
         ios.set_option("verbose", false);
+    if (use_flycheck)
+        ios.set_option("use_flycheck", true);
     script_state S = lean::get_thread_script_state();
     set_environment set1(S, env);
     set_io_state    set2(S, ios);