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

feat(shell/lean): add --line, --col and --goal options for testing Emacs interface

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-24 12:29:31 -07:00
parent c0b4a47f63
commit 1e13f383f6
1 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/shell/lean.cpp
View file

@ -121,6 +121,10 @@ static void display_help(std::ostream & out) {
std::cout << " --tstack=num -s thread stack size in Kb\n";
#endif
std::cout << " -D name=value set a configuration option (see set_option command)\n";
std::cout << "Frontend query interface:\n";
std::cout << " --line=value line number for query\n";
std::cout << " --col=value column number for query\n";
std::cout << " --goal display goal at close to given position\n";
}
static char const * get_file_extension(char const * fname) {
@ -165,10 +169,13 @@ static struct option g_long_options[] = {
#if defined(LEAN_USE_BOOST)
{"tstack", required_argument, 0, 's'},
#endif
{"line", required_argument, 0, 'L'},
{"col", required_argument, 0, 'O'},
{"goal", no_argument, 0, 'G'},
{0, 0, 0, 0}
};
#define OPT_STR "HRXFC:dD:qrlupgvhk:012t:012o:c:i:"
#define OPT_STR "HRXFC:dD:qrlupgvhk:012t:012o:c:i:L:012O:012G"
#if defined(LEAN_TRACK_MEMORY)
#define OPT_STR2 OPT_STR "M:012"
@ -346,6 +353,9 @@ int main(int argc, char ** argv) {
std::string cpp_output;
std::string cache_name;
std::string index_name;
optional<unsigned> line;
optional<unsigned> column;
bool show_goal;
input_kind default_k = input_kind::Unspecified;
while (true) {
int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
@ -435,6 +445,15 @@ int main(int argc, char ** argv) {
case 'F':
opts = opts.update("flycheck", true);
break;
case 'L':
line = atoi(optarg);
break;
case 'O':
column = atoi(optarg);
break;
case 'G':
show_goal = true;
break;
default:
std::cerr << "Unknown command line option\n";
display_help(std::cerr);
@ -442,6 +461,11 @@ int main(int argc, char ** argv) {
}
}
if (show_goal) {
std::cout << "SHOW GOAL @ " << *line << " : " << *column << "\n";
exit(0);
}
#if !defined(LEAN_MULTI_THREAD)
lean_assert(!server);
lean_assert(num_threads == 1);