max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean/parser): remove obsolete option

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-14 09:49:34 +01:00
parent e64c10dd20
commit 98f86ccabd
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -68,10 +68,6 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
#endif
#ifndef LEAN_DEFAULT_PARSER_PARALLEL_IMPORT
#define LEAN_DEFAULT_PARSER_PARALLEL_IMPORT false
#endif
namespace lean {
void break_at_pos_exception::report_goal_pos(pos_info goal_pos) {
@ -82,7 +78,6 @@ void break_at_pos_exception::report_goal_pos(pos_info goal_pos) {
// ==========================================
// Parser configuration options
static name * g_parser_show_errors;
static name * g_parser_parallel_import;
bool get_parser_show_errors(options const & opts) {
return opts.get_bool(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS);
@ -2445,11 +2440,8 @@ bool parse_commands(environment & env, io_state & ios, char const * fname) {
void initialize_parser() {
g_parser_show_errors = new name{"parser", "show_errors"};
g_parser_parallel_import = new name{"parser", "parallel_import"};
register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
"(lean parser) display error messages in the regular output channel");
register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
"(lean parser) import modules in parallel");
g_tmp_prefix = new name(name::mk_internal_unique_name());
g_documentable_cmds = new name_set();
@ -2470,7 +2462,6 @@ void initialize_parser() {
void finalize_parser() {
delete g_tmp_prefix;
delete g_parser_show_errors;
delete g_parser_parallel_import;
delete g_documentable_cmds;
}
}