michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/error_handling): generate valid line and column information

Browse source 
when in flycheck mode
This commit is contained in:
Leonardo de Moura 2014-09-14 20:15:22 -07:00
parent edcbe6fe10
commit 841658ec37
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/error_handling/error_handling.cpp
View file

@ -36,6 +36,13 @@ flyinfo_scope::~flyinfo_scope() {
void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
ios << strm_name << ":";
if (ios.get_options().get_bool("flycheck", false)) {
// generate valid line and column for flycheck mode
if (line == static_cast<unsigned>(-1))
line = 1;
if (pos == static_cast<unsigned>(-1))
pos = 0;
}
if (line != static_cast<unsigned>(-1))
ios << line << ":";
if (pos != static_cast<unsigned>(-1))