michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: add "--flycheck" option to print out error msgs for flycheck

Browse source
This commit is contained in:
Soonho Kong 2014-07-31 11:18:51 -07:00
parent 82afcfac9c
commit 14a406d4d7
3 changed files with 16 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parser.cpp
View file

@ -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) {

3
src/library/error_handling/error_handling.cpp
View file

@ -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;
}
}

12
src/shell/lean.cpp
View file

@ -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);