Support flush at eom to ensure complete output

Author: tautschnig

src/util/cout_message.cpp

@@ -101,30 +101,47 @@ void console_message_handlert::print(
     if(level>=4)
     {
       std::cout << message << '\n';
-
-      if(level<=6)
-        std::cout << std::flush;
     }
     else
-      std::cerr << message << '\n' << std::flush;
+      std::cerr << message << '\n';
   }
   #else
-  // We flush after messages of level 6 or lower.
-  // We don't for messages of level 7 or higher to improve performance,
-  // in particular when writing to NFS.
   // Messages level 3 or lower go to cerr, messages level 4 or
   // above go to cout.
 
   if(level>=4)
   {
     std::cout << message << '\n';
+  }
+  else
+    std::cerr << message << '\n';
+  #endif
+}
+
+/*******************************************************************\
+
+Function: console_message_handlert::flush
 
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void console_message_handlert::flush(unsigned level)
+{
+  // We flush after messages of level 6 or lower.
+  // We don't for messages of level 7 or higher to improve performance,
+  // in particular when writing to NFS.
+  if(level>=4)
+  {
     if(level<=6)
       std::cout << std::flush;
   }
   else
-    std::cerr << message << '\n' << std::flush;
-  #endif
+    std::cerr << std::flush;
 }
 
 /*******************************************************************\

src/util/cout_message.h

@@ -32,6 +32,8 @@ class console_message_handlert:public message_handlert
   virtual void print(
     unsigned level,
     const std::string &message) override;
+
+  virtual void flush(unsigned level) override;
 };
 
 class gcc_message_handlert:public message_handlert

src/util/message.h

@@ -30,6 +30,11 @@ class message_handlert
     int sequence_number,
     const source_locationt &location);
 
+  virtual void flush(unsigned level)
+  {
+    // no-op by default
+  }
+
   virtual ~message_handlert()
   {
   }
@@ -84,6 +89,11 @@ class stream_message_handlert:public message_handlert
     }
   }
 
+  virtual void flush(unsigned level)
+  {
+    out << std::flush;
+  }
+
 protected:
   std::ostream &out;
 };
@@ -216,7 +226,15 @@ class messaget:public message_clientt
   // the printing of the message
   static inline mstreamt &eom(mstreamt &m)
   {
-    m.message.print(m.message_level, m.str(), -1, m.source_location);
+    if(m.message.message_handler)
+    {
+      m.message.message_handler->print(
+        m.message_level,
+        m.str(),
+        -1,
+        m.source_location);
+      m.message.message_handler->flush(m.message_level);
+    }
     m.clear(); // clears error bits
     m.str(std::string()); // clears the string
     m.source_location.clear();

src/util/ui_message.cpp

@@ -323,3 +323,35 @@ void ui_message_handlert::json_ui_msg(
   //  a trailing comma.
   std::cout << ",\n" << result;
 }
+
+/*******************************************************************\
+
+Function: ui_message_handlert::flush
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void ui_message_handlert::flush(unsigned level)
+{
+  switch(get_ui())
+  {
+  case PLAIN:
+  {
+    console_message_handlert console_message_handler;
+    console_message_handler.flush(level);
+  }
+  break;
+
+  case XML_UI:
+  case JSON_UI:
+  {
+    std::cout << std::flush;
+  }
+  break;
+  }
+}

src/util/ui_message.h

@@ -31,6 +31,8 @@ class ui_message_handlert:public message_handlert
     _ui=__ui;
   }
 
+  virtual void flush(unsigned level);
+
 protected:
   uit _ui;