Merge pull request #7186 from diffblue/help-line-breaks

automatically format help text to match terminal width

Author: kroening

src/cprover/console.cpp

@@ -65,6 +65,8 @@ class windows_coutt : public std::streambuf
 bool consolet::_is_terminal = false;
 bool consolet::_use_SGR = false;
 bool consolet::_init_done = false;
+bool consolet::_width_is_set = false;
+std::size_t consolet::_width;
 std::ostream *consolet::_out = nullptr;
 std::ostream *consolet::_err = nullptr;
 
@@ -181,15 +183,19 @@ std::ostream &consolet::reset(std::ostream &str)
 
 std::size_t consolet::width()
 {
-  std::size_t width = 80; // default
+  if(_width_is_set)
+    return _width;
 
-  if(_is_terminal)
+  _width_is_set = true;
+  _width = 80; // default
+
+  if(is_terminal())
   {
 #ifdef _WIN32
     HANDLE h = GetStdHandle(STD_OUTPUT_HANDLE);
     CONSOLE_SCREEN_BUFFER_INFO info;
     GetConsoleScreenBufferInfo(h, &info);
-    width = info.srWindow.Right - info.srWindow.Left + 1;
+    _width = info.srWindow.Right - info.srWindow.Left + 1;
 #else
     std::ostringstream width_stream;
     run("stty", {"stty", "size"}, "", width_stream, "");
@@ -200,12 +206,12 @@ std::size_t consolet::width()
     {
       auto width_l = atol(stty_output[1].c_str());
       if(width_l >= 10 && width_l <= 400)
-        width = width_l;
+        _width = width_l;
     }
 #endif
   }
 
-  return width;
+  return _width;
 }
 
 extern "C" int mk_wcwidth(wchar_t ucs);

src/cprover/console.h

@@ -82,6 +82,8 @@ class consolet
   static bool _is_terminal;
   static bool _use_SGR;
   static bool _init_done;
+  static std::size_t _width;
+  static bool _width_is_set;
   static std::ostream *_out;
   static std::ostream *_err;
 };

src/cprover/cprover_parse_options.cpp

@@ -323,8 +323,8 @@ void cprover_parse_optionst::help()
     " {bcprover} {usource-file.c}    \t convert a given C program\n"
     "\n"
     "Other options:\n"
-    " {y--inline} \t perform function call inlining before\n"
-    " \t generating the formula\n"
+    " {y--inline} \t perform function call inlining before"
+    " generating the formula\n"
     " {y--no-safety} \t disable safety checks\n"
     " {y--contract} {ufunction} \t check contract of given function\n"
     " {y--outfile} {ufile-name} \t set output file for formula\n"

src/cprover/help_formatter.cpp

@@ -12,6 +12,23 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <ostream>
 
+void help_formattert::emit_word(statet &state, std::ostream &out)
+{
+  if(state.word.empty())
+    return;
+
+  // screen width exceeded when aligning?
+  if(state.column + state.word.size() > consolet::width() && state.aligning)
+  {
+    out << '\n' << std::string(first_column_width + 1, ' ');
+    state.column = first_column_width + 1;
+  }
+
+  out << state.word;
+  state.column += state.word.size();
+  state.word.clear();
+}
+
 void help_formattert::operator()(std::ostream &out) const
 {
   std::size_t pos = 0;
@@ -22,15 +39,21 @@ void help_formattert::operator()(std::ostream &out) const
       return 0;
   };
 
-  std::size_t col = 0;
+  statet state;
 
   while(pos < s.size())
   {
     auto ch = next();
 
     if(ch == '{')
     {
+      emit_word(state, out);
+
       auto what = next();
+      // spaces in formatted text are non-breakable
+      while(pos < s.size() && (ch = next()) != '}')
+        state.word += ch;
+
       switch(what)
       {
       case 'b':
@@ -46,31 +69,33 @@ void help_formattert::operator()(std::ostream &out) const
         break;
       }
 
-      while(pos < s.size() && (ch = next()) != '}')
-      {
-        out << ch;
-        col++;
-      }
-
+      emit_word(state, out);
       out << consolet::reset;
     }
     else if(ch == '\t')
     {
-      if(col < 29)
+      emit_word(state, out);
+      if(state.column < first_column_width)
       {
-        out << std::string(29 - col, ' ');
-        col = 40;
+        out << std::string(first_column_width - state.column, ' ');
+        state.column = first_column_width;
       }
+      state.aligning = true;
     }
     else if(ch == '\n')
     {
-      out << ch;
-      col = 0;
+      emit_word(state, out);
+      out << '\n';
+      state.column = 0;
+      state.aligning = false;
     }
     else
     {
-      out << ch;
-      col++;
+      state.word += ch;
+      if(ch == ' ')
+        emit_word(state, out);
     }
   }
+
+  emit_word(state, out);
 }

src/cprover/help_formatter.h

@@ -24,6 +24,17 @@ class help_formattert
 
   const std::string &s;
   void operator()(std::ostream &) const;
+
+protected:
+  struct statet
+  {
+    std::size_t column = 0;
+    bool aligning = false;
+    std::string word = "";
+  };
+
+  static void emit_word(statet &, std::ostream &);
+  static const std::size_t first_column_width = 29;
 };
 
 static inline help_formattert help_formatter(const std::string &s)