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

fix(shell/lean): do not update cache file in query mode

Browse source 
query mode is "show goal" and "show hole" command line options
This commit is contained in:
Leonardo de Moura 2015-07-27 19:00:36 -07:00
parent d50fa26ca2
commit b4504357b2
1 changed files with 10 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/shell/lean.cpp
View file

@ -250,7 +250,8 @@ int main(int argc, char ** argv) {
bool server = false;
bool only_deps = false;
unsigned num_threads = 1;
bool use_cache = false;
bool read_cache = false;
bool save_cache = false;
bool gen_index = false;
keep_theorem_mode tmode = keep_theorem_mode::All;
options opts;
@ -312,7 +313,8 @@ int main(int argc, char ** argv) {
break;
case 'c':
cache_name = optarg;
use_cache = true;
read_cache = true;
save_cache = true;
break;
case 'i':
index_name = optarg;
@ -374,13 +376,15 @@ int main(int argc, char ** argv) {
}
if (show_hole && line && column) {
opts = set_show_hole(opts, *line, *column);
opts = set_show_hole(opts, *line, *column);
save_cache = false;
}
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
if (show_goal && line && column) {
opts = set_show_goal(opts, *line, *column);
opts = set_show_goal(opts, *line, *column);
save_cache = false;
}
#if !defined(LEAN_MULTI_THREAD)
@ -423,7 +427,7 @@ int main(int argc, char ** argv) {
set_io_state set2(S, ios);
definition_cache cache;
definition_cache * cache_ptr = nullptr;
if (use_cache) {
if (read_cache) {
try {
cache_ptr = &cache;
std::ifstream in(cache_name, std::ifstream::binary);
@ -497,7 +501,7 @@ int main(int argc, char ** argv) {
if (!Sv(std::cin))
ok = false;
}
if (use_cache) {
if (save_cache) {
std::ofstream out(cache_name, std::ofstream::binary);
cache.save(out);
}