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

fix(shell/lean,library/messages): print messages in correct order (and immediately) when --json was not given

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-01 17:10:14 +01:00
parent 7dc4d4e5fa
commit 64ab576dbf
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/messages.cpp
View file

@ -6,6 +6,7 @@ Author: Gabriel Ebner
*/
#include <string>
#include "library/messages.h"
#include "library/trace.h"
namespace lean {
@ -31,6 +32,10 @@ std::ostream & operator<<(std::ostream & out, message const & msg) {
}
void report_message(message const & msg0) {
if (!get_global_ios().get_options().get_bool(name {"trace", "as_messages"}, false)) {
// Print immediately. Still add as a message so that we get the error code correct.
get_global_ios().get_regular_stream() << msg0;
}
lean_assert(global_message_log());
global_message_log()->add(msg0);
}

8
src/shell/lean.cpp
View file

@ -498,14 +498,14 @@ int main(int argc, char ** argv) {
write_module(p.env(), mod_fn, olean_fn);
}
for (auto const & msg : l.to_buffer()) {
if (json_output) {
if (json_output) {
#if defined(LEAN_JSON)
for (auto const & msg : l.to_buffer()) {
print_json(std::cout, msg);
#endif
} else {
std::cout << msg;
}
} else {
// Messages have already been printed directly to stdout
}
if (!json_output)