From 69750c50c61bc8370dfe523f435ae1ee1e9dc242 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Dec 2014 15:00:05 -0800 Subject: [PATCH] refactor(frontends/lean): move pp_options to library --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/info_manager.cpp | 2 +- src/frontends/lean/init_module.cpp | 3 --- src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/placeholder_elaborator.cpp | 2 +- src/frontends/lean/pp.cpp | 2 +- src/library/CMakeLists.txt | 2 +- src/library/init_module.cpp | 3 +++ src/{frontends/lean => library}/pp_options.cpp | 2 +- src/{frontends/lean => library}/pp_options.h | 0 12 files changed, 12 insertions(+), 12 deletions(-) rename src/{frontends/lean => library}/pp_options.cpp (99%) rename src/{frontends/lean => library}/pp_options.h (100%) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index b742b6b58..8d823dd71 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -3,7 +3,7 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp -begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp +begin_end_ext.cpp class.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index d0fb5a753..7fd0278a6 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/class.h" #include "library/flycheck.h" #include "library/util.h" +#include "library/pp_options.h" #include "library/definitional/projection.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" @@ -37,7 +38,6 @@ Author: Leonardo de Moura #include "frontends/lean/class.h" #include "frontends/lean/tactic_hint.h" #include "frontends/lean/tokens.h" -#include "frontends/lean/pp_options.h" #include "frontends/lean/parse_table.h" namespace lean { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1d4023a64..4aae8ec83 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "library/local_context.h" #include "library/util.h" #include "library/choice_iterator.h" +#include "library/pp_options.h" #include "library/tactic/expr_to_tactic.h" #include "library/error_handling/error_handling.h" #include "library/definitional/equations.h" @@ -47,7 +48,6 @@ Author: Leonardo de Moura #include "frontends/lean/proof_qed_elaborator.h" #include "frontends/lean/calc_proof_elaborator.h" #include "frontends/lean/info_tactic.h" -#include "frontends/lean/pp_options.h" #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/elaborator_exception.h" #include "frontends/lean/calc.h" diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 1610a2f89..fe99fd589 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -11,10 +11,10 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "library/choice.h" #include "library/scoped_ext.h" +#include "library/pp_options.h" #include "library/tactic/proof_state.h" #include "library/tactic/expr_to_tactic.h" #include "frontends/lean/info_manager.h" -#include "frontends/lean/pp_options.h" namespace lean { class info_data; diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 60d804c23..bb59d8d4a 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -7,7 +7,6 @@ Author: Leonardo de Moura #include "frontends/lean/tokens.h" #include "frontends/lean/elaborator_context.h" #include "frontends/lean/elaborator.h" -#include "frontends/lean/pp_options.h" #include "frontends/lean/parser.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/tactic_hint.h" @@ -39,7 +38,6 @@ void initialize_frontend_lean_module() { initialize_builtin_exprs(); initialize_elaborator_context(); initialize_elaborator(); - initialize_pp_options(); initialize_scanner(); initialize_parser(); initialize_tactic_hint(); @@ -72,7 +70,6 @@ void finalize_frontend_lean_module() { finalize_tactic_hint(); finalize_parser(); finalize_scanner(); - finalize_pp_options(); finalize_elaborator(); finalize_elaborator_context(); finalize_builtin_exprs(); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3569061f9..bb5233641 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "library/string.h" #include "library/sorry.h" #include "library/flycheck.h" +#include "library/pp_options.h" #include "library/error_handling/error_handling.h" #include "library/tactic/expr_to_tactic.h" #include "frontends/lean/tokens.h" @@ -41,7 +42,6 @@ Author: Leonardo de Moura #include "frontends/lean/parser_bindings.h" #include "frontends/lean/notation_cmd.h" #include "frontends/lean/elaborator.h" -#include "frontends/lean/pp_options.h" #include "frontends/lean/info_annotation.h" #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index f70978bed..f3659bc59 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -18,9 +18,9 @@ Author: Leonardo de Moura #include "library/class.h" #include "library/local_context.h" #include "library/choice_iterator.h" +#include "library/pp_options.h" #include "frontends/lean/util.h" #include "frontends/lean/elaborator_exception.h" -#include "frontends/lean/pp_options.h" #ifndef LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES #define LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES false diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 18c0eb2b0..b8a65afe9 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -23,8 +23,8 @@ Author: Leonardo de Moura #include "library/num.h" #include "library/let.h" #include "library/print.h" +#include "library/pp_options.h" #include "frontends/lean/pp.h" -#include "frontends/lean/pp_options.h" #include "frontends/lean/token_table.h" #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/parser_config.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index db4e9535a..18e3922a2 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -11,6 +11,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp - local_context.cpp choice_iterator.cpp) + local_context.cpp choice_iterator.cpp pp_options.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 0b5c9da50..67393561b 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "library/print.h" #include "library/fingerprint.h" #include "library/util.h" +#include "library/pp_options.h" namespace lean { void initialize_library_module() { @@ -61,9 +62,11 @@ void initialize_library_module() { initialize_sorry(); initialize_class(); initialize_library_util(); + initialize_pp_options(); } void finalize_library_module() { + finalize_pp_options(); finalize_library_util(); finalize_class(); finalize_sorry(); diff --git a/src/frontends/lean/pp_options.cpp b/src/library/pp_options.cpp similarity index 99% rename from src/frontends/lean/pp_options.cpp rename to src/library/pp_options.cpp index bb7d32b04..399b680cc 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sexpr/option_declarations.h" -#include "frontends/lean/pp_options.h" +#include "library/pp_options.h" #ifndef LEAN_DEFAULT_PP_MAX_DEPTH #define LEAN_DEFAULT_PP_MAX_DEPTH 1000000 diff --git a/src/frontends/lean/pp_options.h b/src/library/pp_options.h similarity index 100% rename from src/frontends/lean/pp_options.h rename to src/library/pp_options.h