From a005c8f4d03052268e39664a26e840287d1b3a40 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Nov 2014 08:35:49 -0800 Subject: [PATCH] feat(frontends/lean): display eval/check/find_decl results using flycheck --- src/emacs/lean-flycheck.el | 5 +++++ src/frontends/lean/builtin_cmds.cpp | 11 +++++++++++ src/frontends/lean/find_cmd.cpp | 5 +++++ src/frontends/lean/parser.cpp | 4 ++++ src/frontends/lean/parser.h | 1 + src/library/error_handling/error_handling.cpp | 5 +++++ src/library/error_handling/error_handling.h | 1 + src/library/flycheck.cpp | 9 --------- src/library/flycheck.h | 9 +++------ 9 files changed, 35 insertions(+), 15 deletions(-) diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el index a4c672878..671731966 100644 --- a/src/emacs/lean-flycheck.el +++ b/src/emacs/lean-flycheck.el @@ -34,6 +34,11 @@ (minimal-match (message (one-or-more (zero-or-more not-newline) (? "\r") "\n"))) "FLYCHECK_END" (? "\r") line-end) + (warning line-start "FLYCHECK_BEGIN INFORMATION" (? "\r") "\n" + (file-name) ":" line ":" (? column ":") " information: " + (minimal-match + (message (one-or-more (zero-or-more not-newline) (? "\r") "\n"))) + "FLYCHECK_END" (? "\r") line-end) (warning line-start "FLYCHECK_BEGIN WARNING" (? "\r") "\n" (file-name) ":" line ":" (? column ":") " warning: " (minimal-match diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index ed5f21618..865f678b3 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/normalize.h" #include "library/print.h" +#include "library/flycheck.h" #include "library/definitional/projection.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" @@ -252,6 +253,11 @@ environment check_cmd(parser & p) { fmt = fmt.update_options(opts); unsigned indent = get_pp_indent(opts); format r = group(fmt(e) + space() + colon() + nest(indent, line() + fmt(type))); + flycheck_information info(p.regular_stream()); + if (info.enabled()) { + p.display_information_pos(p.cmd_pos()); + p.regular_stream() << "check result:\n"; + } reg << mk_pair(r, opts) << endl; return p.env(); } @@ -278,6 +284,11 @@ environment eval_cmd(parser & p) { transparent_scope scope; r = normalize(p.env(), ls, e); } + flycheck_information info(p.regular_stream()); + if (info.enabled()) { + p.display_information_pos(p.cmd_pos()); + p.regular_stream() << "eval result:\n"; + } p.regular_stream() << r << endl; return p.env(); } diff --git a/src/frontends/lean/find_cmd.cpp b/src/frontends/lean/find_cmd.cpp index 3d5da4aac..11ee1b819 100644 --- a/src/frontends/lean/find_cmd.cpp +++ b/src/frontends/lean/find_cmd.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/type_util.h" #include "library/reducible.h" +#include "library/flycheck.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/tokens.h" @@ -102,6 +103,10 @@ environment find_cmd(parser & p) { parse_filters(p, pos_names, neg_names); environment env = p.env(); auto tc = mk_opaque_type_checker(env, p.mk_ngen()); + flycheck_information info(p.regular_stream()); + if (info.enabled()) { + p.display_information_pos(p.cmd_pos()); + } p.regular_stream() << "find_decl result:\n"; unsigned max_steps = get_find_max_steps(p.get_options()); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c435f1d01..ad6d791b1 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -212,6 +212,10 @@ void parser::display_warning_pos(unsigned line, unsigned pos) { } void parser::display_warning_pos(pos_info p) { display_warning_pos(p.first, p.second); } +void parser::display_information_pos(pos_info pos) { + ::lean::display_information_pos(regular_stream(), get_stream_name().c_str(), pos.first, pos.second); +} + void parser::display_error_pos(unsigned line, unsigned pos) { ::lean::display_error_pos(regular_stream(), get_stream_name().c_str(), line, pos); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 3eb065f61..c2433bd9c 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -415,6 +415,7 @@ public: void declare_sorry(); parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); } + void display_information_pos(pos_info p); /** parse all commands in the input stream */ bool operator()() { return parse_commands(); } diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 53654edc9..20dec1fa7 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -42,6 +42,11 @@ void display_warning_pos(io_state_stream const & ios, char const * strm_name, un ios << " warning:"; } +void display_information_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) { + display_pos(ios, strm_name, line, pos); + ios << " information:"; +} + void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, expr const & e) { if (p) { auto pos = p->get_pos_info_or_some(e); diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling/error_handling.h index 6d1aed00d..336718a5d 100644 --- a/src/library/error_handling/error_handling.h +++ b/src/library/error_handling/error_handling.h @@ -19,6 +19,7 @@ void display_error_pos(io_state_stream const & ios, pos_info_provider const * p, void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos); /** \brief Similar to #display_error_pos, but displays a "warning:" */ void display_warning_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos); +void display_information_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos); /** \brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios. Exceptions that contain expressions use the given \c pos_info_provider (if available) to retrieve line number information. diff --git a/src/library/flycheck.cpp b/src/library/flycheck.cpp index a66aa670c..232a1a84c 100644 --- a/src/library/flycheck.cpp +++ b/src/library/flycheck.cpp @@ -15,13 +15,4 @@ flycheck_scope::flycheck_scope(io_state_stream const & ios, char const * kind): flycheck_scope::~flycheck_scope() { if (m_flycheck) m_ios << "FLYCHECK_END" << endl; } - -flyinfo_scope::flyinfo_scope(io_state_stream const & ios): - m_ios(ios), - m_flyinfo(m_ios.get_options().get_bool("flyinfo", false)) { - if (m_flyinfo) m_ios << "FLYCHECK_BEGIN INFO" << endl; -} -flyinfo_scope::~flyinfo_scope() { - if (m_flyinfo) m_ios << "FLYCHECK_END" << endl; -} } diff --git a/src/library/flycheck.h b/src/library/flycheck.h index 7716bb937..fcac082b1 100644 --- a/src/library/flycheck.h +++ b/src/library/flycheck.h @@ -15,6 +15,7 @@ class flycheck_scope { public: flycheck_scope(io_state_stream const & ios, char const * kind); ~flycheck_scope(); + bool enabled() const { return m_flycheck; } }; struct flycheck_error : public flycheck_scope { @@ -25,11 +26,7 @@ struct flycheck_warning : public flycheck_scope { flycheck_warning(io_state_stream const & ios):flycheck_scope(ios, "WARNING") {} }; -class flyinfo_scope { - io_state_stream const & m_ios; - bool m_flyinfo; -public: - flyinfo_scope(io_state_stream const & ios); - ~flyinfo_scope(); +struct flycheck_information : public flycheck_scope { + flycheck_information(io_state_stream const & ios):flycheck_scope(ios, "INFORMATION") {} }; }