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

feat(library/flycheck,frontends/lean/elaborator): show trace messages in flycheck

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-04 15:47:05 -04:00 • committed by Leonardo de Moura
parent 6883720cc7
commit 996b4375a9
3 changed files with 48 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -2297,6 +2297,9 @@ void elaborator::show_goal(tactic_state const & s, expr const & start_ref, expr
/* Apply the given tactic to the state 's'.
Report any errors detected during the process using position information associated with 'ref'. */
tactic_state elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
pos_info_provider * provider = get_pos_info_provider();
flycheck_output_scope flycheck(provider, ref);
/* Compile tactic into bytecode */
name tactic_name("_tactic");
expr tactic_type = mk_tactic_unit();
@ -2318,7 +2321,6 @@ tactic_state elaborator::execute_tactic(expr const & tactic, tactic_state const
format fmt = std::get<0>(*ex);
optional<expr> ref1 = std::get<1>(*ex);
tactic_state s1 = std::get<2>(*ex);
pos_info_provider * provider = get_pos_info_provider();
if (ref1 && provider && provider->get_pos_info(*ref1))
throw elaborator_exception(*ref1, fmt);
else

29
src/library/flycheck.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/flycheck.h"
#include "library/error_handling.h"
namespace lean {
flycheck_scope::flycheck_scope(std::ostream & out, options const & o, char const * kind):
@ -15,4 +16,32 @@ flycheck_scope::flycheck_scope(std::ostream & out, options const & o, char const
flycheck_scope::~flycheck_scope() {
if (m_flycheck) m_out << "FLYCHECK_END" << std::endl;
}
flycheck_output_scope::flycheck_output_scope(io_state const & ios, char const * stream_name, pos_info const & pos) :
m_stream_name(stream_name), m_pos(pos),
m_out(ios.get_regular_stream()),
m_redirected_ios(ios),
m_scoped_ios(), m_buffer() {
if (ios.get_options().get_bool("flycheck", false)) {
m_buffer = std::shared_ptr<string_output_channel>(new string_output_channel);
m_redirected_ios.set_diagnostic_channel(m_buffer);
m_redirected_ios.set_regular_channel(m_buffer);
m_scoped_ios = std::unique_ptr<scope_global_ios>(new scope_global_ios(m_redirected_ios));
lean_assert(enabled());
}
}
flycheck_output_scope::flycheck_output_scope(pos_info_provider const * provider, expr const & ref) :
flycheck_output_scope(get_global_ios(),
provider ? provider->get_file_name() : "unknown",
provider ? provider->get_pos_info_or_some(ref) : pos_info(0, 0)) {}
flycheck_output_scope::~flycheck_output_scope() {
if (enabled()) {
auto redirected_output = m_buffer->str();
if (!redirected_output.empty()) {
m_out << "FLYCHECK_BEGIN INFORMATION" << std::endl;
display_pos(m_out, m_stream_name, m_pos.first, m_pos.second);
m_out << " information:" << std::endl << redirected_output;
m_out << "FLYCHECK_END" << std::endl;
}
}
}
}

16
src/library/flycheck.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include <iostream>
#include "kernel/pos_info_provider.h"
#include "util/sexpr/options.h"
#include "library/io_state.h"
@ -22,6 +23,21 @@ public:
bool enabled() const { return m_flycheck; }
};
/** Redirects regular and diagnostic output streams of the global ios as flycheck informations. */
class flycheck_output_scope {
char const * m_stream_name;
pos_info m_pos;
std::ostream & m_out;
io_state m_redirected_ios;
std::unique_ptr<scope_global_ios> m_scoped_ios;
std::shared_ptr<string_output_channel> m_buffer;
public:
flycheck_output_scope(io_state const & ios, char const * stream_name, pos_info const & pos);
flycheck_output_scope(pos_info_provider const * provider, expr const & ref);
~flycheck_output_scope();
bool enabled() const { return static_cast<bool>(m_scoped_ios); }
};
struct flycheck_error : public flycheck_scope {
flycheck_error(std::ostream & out, options const & o):flycheck_scope(out, o, "ERROR") {}
flycheck_error(io_state const & ios):flycheck_scope(ios, "ERROR") {}