From 64ab576dbf4e656897766e376b91f67a2247772b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 1 Feb 2019 17:10:14 +0100
Subject: [PATCH] fix(shell/lean,library/messages): print messages in correct
 order (and immediately) when --json was not given

---
 src/library/messages.cpp | 5 +++++
 src/shell/lean.cpp       | 8 ++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/library/messages.cpp b/src/library/messages.cpp
index 28399eca13..2694e73578 100644
--- a/src/library/messages.cpp
+++ b/src/library/messages.cpp
@@ -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);
 }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index ae8280e4f7..d830d46e93 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -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)