From b92416d66c94e1dcb8bffc0dbd34b22175b053f6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Dec 2015 15:31:40 -0800 Subject: [PATCH] refactor(library/error_handling): move error_handling to library main dir --- src/CMakeLists.txt | 2 -- src/api/exception.cpp | 2 +- src/api/ios.cpp | 2 +- src/frontends/lean/decl_cmds.cpp | 2 +- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/parser.cpp | 2 +- src/library/CMakeLists.txt | 2 +- src/library/{error_handling => }/error_handling.cpp | 2 +- src/library/{error_handling => }/error_handling.h | 0 src/library/error_handling/CMakeLists.txt | 1 - src/shell/emscripten.cpp | 2 +- src/shell/lean.cpp | 2 +- 12 files changed, 9 insertions(+), 12 deletions(-) rename src/library/{error_handling => }/error_handling.cpp (99%) rename src/library/{error_handling => }/error_handling.h (100%) delete mode 100644 src/library/error_handling/CMakeLists.txt diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a2b11b0c5..60fa662fe 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -361,8 +361,6 @@ add_subdirectory(library/blast/grinder) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/blast/simplifier) set(LEAN_OBJS ${LEAN_OBJS} $) -add_subdirectory(library/error_handling) -set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(compiler) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(frontends/lean) diff --git a/src/api/exception.cpp b/src/api/exception.cpp index 7d0f11f0b..b35265f4a 100644 --- a/src/api/exception.cpp +++ b/src/api/exception.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/print.h" #include "library/tactic/tactic.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "api/exception.h" #include "api/string.h" using namespace lean; // NOLINT diff --git a/src/api/ios.cpp b/src/api/ios.cpp index cad0f1744..9cf263960 100644 --- a/src/api/ios.cpp +++ b/src/api/ios.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "frontends/lean/pp.h" #include "api/string.h" #include "api/exception.h" diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index dc023176d..8d4e10eaa 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -22,7 +22,7 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/abbreviation.h" #include "library/definitional/equations.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/tokens.h" diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d9ad2dd3b..0fc8d66e3 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -41,7 +41,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/class_instance_resolution.h" #include "library/tactic/expr_to_tactic.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "library/definitional/equations.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/structure_cmd.h" diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3898ec49c..26679f6d1 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -41,7 +41,7 @@ Author: Leonardo de Moura #include "library/flycheck.h" #include "library/pp_options.h" #include "library/noncomputable.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/location.h" #include "frontends/lean/tokens.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index c7d80ee59..c085c6e10 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -19,4 +19,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp - attribute_manager.cpp) + attribute_manager.cpp error_handling.cpp) diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling.cpp similarity index 99% rename from src/library/error_handling/error_handling.cpp rename to src/library/error_handling.cpp index 2cc6e1a26..996fc6cee 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling.cpp @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "library/parser_nested_exception.h" #include "library/flycheck.h" #include "library/pp_options.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" namespace lean { void display_pos(std::ostream & out, options const & o, char const * strm_name, unsigned line, unsigned pos) { diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling.h similarity index 100% rename from src/library/error_handling/error_handling.h rename to src/library/error_handling.h diff --git a/src/library/error_handling/CMakeLists.txt b/src/library/error_handling/CMakeLists.txt deleted file mode 100644 index 967083526..000000000 --- a/src/library/error_handling/CMakeLists.txt +++ /dev/null @@ -1 +0,0 @@ -add_library(error_handling OBJECT error_handling.cpp) diff --git a/src/shell/emscripten.cpp b/src/shell/emscripten.cpp index 6d8c313a1..bc2fe99ce 100644 --- a/src/shell/emscripten.cpp +++ b/src/shell/emscripten.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/standard_kernel.h" #include "library/kernel_bindings.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "frontends/lean/pp.h" #include "frontends/lean/parser.h" #include "init/init.h" diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index c12c498c9..43d759ae3 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -34,7 +34,7 @@ Author: Leonardo de Moura #include "library/definition_cache.h" #include "library/declaration_index.h" #include "library/export.h" -#include "library/error_handling/error_handling.h" +#include "library/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/pp.h" #include "frontends/lean/server.h"