automatically format help text to match terminal width

This extends the help formatter used by the CHC encoder to consider the
width of the terminal when formatting the command line help.  Lines are
wrapped on spaces that are encountered in non-highlighted text.

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)