Revert 20e4def (preformatted_output flag)

peterschrammel · peterschrammel · commit 5ef9c17dc4b3 · 2017-09-15T23:56:35.000+01:00
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -64,7 +64,7 @@ void bmct::error_trace()
     {
       xmlt xml;
       convert(ns, goto_trace, xml);
-      status() << preformatted_output << xml << eom;
+      status() << xml << eom;
     }
     break;
 
@@ -81,7 +81,7 @@ void bmct::error_trace()
       result["status"]=json_stringt("failed");
       jsont &json_trace=result["trace"];
       convert(ns, goto_trace, json_trace);
-      status() << preformatted_output << json_result << eom;
+      status() << ",\n" << json_result << eom;
     }
     break;
   }
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
@@ -31,10 +31,9 @@ cerr_message_handlert::cerr_message_handlert():
 
 void console_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   if(verbosity<level)
     return;
@@ -102,8 +101,7 @@ void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   const irep_idt file=location.get_file();
   const irep_idt line=location.get_line();
@@ -141,15 +139,14 @@ void gcc_message_handlert::print(
 
   dest+=message;
 
-  print(level, dest, preformatted);
+  print(level, dest);
 }
 
 void gcc_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   // gcc appears to send everything to cerr
   if(verbosity>=level)
diff --git a/src/util/cout_message.h b/src/util/cout_message.h
@@ -32,8 +32,7 @@ class console_message_handlert:public ui_message_handlert
   // level 4 and upwards go to cout, level 1-3 to cerr
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted) override;
+    const std::string &message) override;
 
   virtual void flush(unsigned level) override;
 };
@@ -44,15 +43,13 @@ class gcc_message_handlert:public ui_message_handlert
   // aims to imitate the messages gcc prints
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted) override;
+    const std::string &message) override;
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted) override;
+    const source_locationt &location) override;
 };
 
 #endif // CPROVER_UTIL_COUT_MESSAGE_H
diff --git a/src/util/message.cpp b/src/util/message.cpp
@@ -13,8 +13,7 @@ void message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   std::string dest;
 
@@ -52,13 +51,12 @@ void message_handlert::print(
     dest+=": ";
   dest+=message;
 
-  print(level, dest, preformatted);
+  print(level, dest);
 }
 
 void message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
   if(level>=message_count.size())
     message_count.resize(level+1, 0);
diff --git a/src/util/message.h b/src/util/message.h
@@ -24,17 +24,13 @@ class message_handlert
   {
   }
 
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    bool preformatted) = 0;
+  virtual void print(unsigned level, const std::string &message) = 0;
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void flush(unsigned level)
   {
@@ -64,22 +60,18 @@ class message_handlert
 class null_message_handlert:public message_handlert
 {
 public:
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    bool preformatted)
+  virtual void print(unsigned level, const std::string &message)
   {
-    message_handlert::print(level, message, preformatted);
+    message_handlert::print(level, message);
   }
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted)
+    const source_locationt &location)
   {
-    print(level, message, preformatted);
+    print(level, message);
   }
 };
 
@@ -90,12 +82,9 @@ class stream_message_handlert:public message_handlert
   {
   }
 
-  virtual void print(
-    unsigned level,
-    const std::string &message,
-    bool preformatted)
+  virtual void print(unsigned level, const std::string &message)
   {
-    message_handlert::print(level, message, preformatted);
+    message_handlert::print(level, message);
 
     if(verbosity>=level)
       out << message << '\n';
@@ -172,23 +161,20 @@ class messaget
       unsigned _message_level,
       messaget &_message):
       message_level(_message_level),
-      message(_message),
-      preformatted(false)
+      message(_message)
     {
     }
 
     mstreamt(const mstreamt &other):
       message_level(other.message_level),
       message(other.message),
-      source_location(other.source_location),
-      preformatted(false)
+      source_location(other.source_location)
     {
     }
 
     unsigned message_level;
     messaget &message;
     source_locationt source_location;
-    bool preformatted;
 
     template <class T>
     mstreamt &operator << (const T &x)
@@ -214,23 +200,15 @@ class messaget
         m.message_level,
         m.str(),
         -1,
-        m.source_location,
-        m.preformatted);
+        m.source_location);
       m.message.message_handler->flush(m.message_level);
     }
-    m.preformatted=false;
     m.clear(); // clears error bits
     m.str(std::string()); // clears the string
     m.source_location.clear();
     return m;
   }
 
-  static mstreamt &preformatted_output(mstreamt &m)
-  {
-    m.preformatted=true;
-    return m;
-  }
-
   // in lieu of std::endl
   static mstreamt &endl(mstreamt &m)
   {
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
@@ -90,8 +90,7 @@ const char *ui_message_handlert::level_string(unsigned level)
 
 void ui_message_handlert::print(
   unsigned level,
-  const std::string &message,
-  bool preformatted)
+  const std::string &message)
 {
   if(verbosity>=level)
   {
@@ -100,7 +99,7 @@ void ui_message_handlert::print(
     case uit::PLAIN:
     {
       console_message_handlert console_message_handler;
-      console_message_handler.print(level, message, preformatted);
+      console_message_handler.print(level, message);
     }
     break;
 
@@ -109,7 +108,7 @@ void ui_message_handlert::print(
     {
       source_locationt location;
       location.make_nil();
-      print(level, message, -1, location, preformatted);
+      print(level, message, -1, location);
     }
     break;
     }
@@ -120,18 +119,17 @@ void ui_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
-  message_handlert::print(level, message, preformatted);
+  message_handlert::print(level, message);
 
   if(verbosity>=level)
   {
     switch(get_ui())
     {
     case uit::PLAIN:
       message_handlert::print(
-        level, message, sequence_number, location, preformatted);
+        level, message, sequence_number, location);
       break;
 
     case uit::XML_UI:
@@ -147,7 +145,7 @@ void ui_message_handlert::print(
       std::string sequence_number_str=
         sequence_number>=0?std::to_string(sequence_number):"";
 
-      ui_msg(type, tmp_message, sequence_number_str, location, preformatted);
+      ui_msg(type, tmp_message, sequence_number_str, location);
     }
     break;
     }
@@ -158,20 +156,19 @@ void ui_message_handlert::ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
   switch(get_ui())
   {
   case uit::PLAIN:
     break;
 
   case uit::XML_UI:
-    xml_ui_msg(type, msg1, msg2, location, preformatted);
+    xml_ui_msg(type, msg1, msg2, location);
     break;
 
   case uit::JSON_UI:
-    json_ui_msg(type, msg1, msg2, location, preformatted);
+    json_ui_msg(type, msg1, msg2, location);
     break;
   }
 }
@@ -180,16 +177,8 @@ void ui_message_handlert::xml_ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
-  if(preformatted)
-  {
-    // Expect the message is already an XML fragment.
-    std::cout << msg1 << '\n';
-    return;
-  }
-
   xmlt result;
   result.name="message";
 
@@ -208,16 +197,8 @@ void ui_message_handlert::json_ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location,
-  bool preformatted)
+  const source_locationt &location)
 {
-  if(preformatted)
-  {
-    // Expect the message is already a JSON fragment.
-    std::cout << ",\n" << msg1;
-    return;
-  }
-
   json_objectt result;
 
   if(location.is_not_nil() &&
diff --git a/src/util/ui_message.h b/src/util/ui_message.h
@@ -44,37 +44,32 @@ class ui_message_handlert:public message_handlert
   // overloading
   virtual void print(
     unsigned level,
-    const std::string &message,
-    bool preformatted);
+    const std::string &message);
 
   // overloading
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void xml_ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void json_ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   virtual void ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location,
-    bool preformatted);
+    const source_locationt &location);
 
   const char *level_string(unsigned level);
 };

Original file line number	Diff line number	Diff line change
`@@ -64,7 +64,7 @@ void bmct::error_trace()`
`64`	`64`	`{`
`65`	`65`	`xmlt xml;`
`66`	`66`	`convert(ns, goto_trace, xml);`
`67`		`- status() << preformatted_output << xml << eom;`
	`67`	`+ status() << xml << eom;`
`68`	`68`	`}`
`69`	`69`	`break;`
`70`	`70`
`@@ -81,7 +81,7 @@ void bmct::error_trace()`
`81`	`81`	`result["status"]=json_stringt("failed");`
`82`	`82`	`jsont &json_trace=result["trace"];`
`83`	`83`	`convert(ns, goto_trace, json_trace);`
`84`		`- status() << preformatted_output << json_result << eom;`
	`84`	`+ status() << ",\n" << json_result << eom;`
`85`	`85`	`}`
`86`	`86`	`break;`
`87`	`87`	`}`