Skip to content

Commit 284733e

Browse files
committed
new help formatter and console API
This commit adds a new help formatter, which supports a limited form of markup to visually distinguish different syntactic elements of the command line arguments. Rendering of the syntax highlighting is done via a new console API.
1 parent e64de21 commit 284733e

File tree

5 files changed

+448
-0
lines changed

5 files changed

+448
-0
lines changed

Diff for: src/util/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ SRC = arith_tools.cpp \
88
c_types.cpp \
99
cmdline.cpp \
1010
config.cpp \
11+
console.cpp \
1112
cout_message.cpp \
1213
dstring.cpp \
1314
endianness_map.cpp \
@@ -28,6 +29,7 @@ SRC = arith_tools.cpp \
2829
fresh_symbol.cpp \
2930
get_base_name.cpp \
3031
get_module.cpp \
32+
help_formatter.cpp \
3133
identifier.cpp \
3234
ieee_float.cpp \
3335
interval_union.cpp \

Diff for: src/util/console.cpp

+229
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,229 @@
1+
/*******************************************************************\
2+
3+
Module: Console
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "console.h"
10+
11+
#include <cctype>
12+
#include <iostream>
13+
#include <sstream>
14+
15+
#ifdef _WIN32
16+
# include <io.h>
17+
# include <windows.h>
18+
# define isatty _isatty
19+
#else
20+
# include <unistd.h>
21+
#endif
22+
23+
#include <util/run.h>
24+
#include <util/string_utils.h>
25+
#include <util/unicode.h>
26+
27+
#ifdef _WIN32
28+
class windows_coutt : public std::streambuf
29+
{
30+
public:
31+
// this turns UTF8 into Windows UTF16
32+
std::streamsize xsputn(const char_type *s, std::streamsize n) override
33+
{
34+
if(consolet::is_terminal())
35+
{
36+
auto wide_string = widen(std::string(s, n));
37+
DWORD number_written;
38+
HANDLE h = GetStdHandle(STD_OUTPUT_HANDLE);
39+
WriteConsoleW(
40+
h,
41+
wide_string.c_str(),
42+
(DWORD)wide_string.size(),
43+
&number_written,
44+
nullptr);
45+
}
46+
else
47+
{
48+
std::cout.write(s, n);
49+
}
50+
51+
return n;
52+
}
53+
54+
int_type overflow(int_type c) override
55+
{
56+
if(consolet::is_terminal())
57+
std::wcout << wchar_t(c);
58+
else
59+
std::cout << char(c);
60+
return wchar_t(c);
61+
}
62+
} windows_cout;
63+
#endif
64+
65+
bool consolet::_is_terminal = false;
66+
bool consolet::_use_SGR = false;
67+
bool consolet::_init_done = false;
68+
std::ostream *consolet::_out = nullptr;
69+
std::ostream *consolet::_err = nullptr;
70+
71+
void consolet::init()
72+
{
73+
if(_init_done)
74+
return;
75+
76+
_init_done = true;
77+
_is_terminal = isatty(1);
78+
79+
_out = &std::cout;
80+
_err = &std::cerr;
81+
82+
#ifdef _WIN32
83+
if(_is_terminal)
84+
{
85+
HANDLE out_handle = GetStdHandle(STD_OUTPUT_HANDLE);
86+
87+
DWORD consoleMode;
88+
if(GetConsoleMode(out_handle, &consoleMode))
89+
{
90+
consoleMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING;
91+
if(SetConsoleMode(out_handle, consoleMode))
92+
_use_SGR = true;
93+
}
94+
95+
std::cout.rdbuf(&windows_cout);
96+
}
97+
#else
98+
_use_SGR = true;
99+
#endif
100+
}
101+
102+
std::ostream &consolet::blue(std::ostream &str)
103+
{
104+
if(is_terminal() && use_SGR())
105+
return str << "\x1b[34m";
106+
else
107+
return str;
108+
}
109+
110+
std::ostream &consolet::cyan(std::ostream &str)
111+
{
112+
if(is_terminal() && use_SGR())
113+
return str << "\x1b[36m";
114+
else
115+
return str;
116+
}
117+
118+
std::ostream &consolet::green(std::ostream &str)
119+
{
120+
if(is_terminal() && use_SGR())
121+
return str << "\x1b[32m";
122+
else
123+
return str;
124+
}
125+
126+
std::ostream &consolet::red(std::ostream &str)
127+
{
128+
if(is_terminal() && use_SGR())
129+
return str << "\x1b[31m";
130+
else
131+
return str;
132+
}
133+
134+
std::ostream &consolet::yellow(std::ostream &str)
135+
{
136+
if(is_terminal() && use_SGR())
137+
return str << "\x1b[33m";
138+
else
139+
return str;
140+
}
141+
142+
std::ostream &consolet::orange(std::ostream &str)
143+
{
144+
if(is_terminal() && use_SGR())
145+
return str << "\x1b[38;5;214m";
146+
else
147+
return str;
148+
}
149+
150+
std::ostream &consolet::bold(std::ostream &str)
151+
{
152+
if(is_terminal() && use_SGR())
153+
return str << "\x1b[1m";
154+
else
155+
return str;
156+
}
157+
158+
std::ostream &consolet::faint(std::ostream &str)
159+
{
160+
if(is_terminal() && use_SGR())
161+
return str << "\x1b[2m";
162+
else
163+
return str;
164+
}
165+
166+
std::ostream &consolet::underline(std::ostream &str)
167+
{
168+
if(is_terminal() && use_SGR())
169+
return str << "\x1b[4m";
170+
else
171+
return str;
172+
}
173+
174+
std::ostream &consolet::reset(std::ostream &str)
175+
{
176+
if(is_terminal() && use_SGR())
177+
return str << "\x1b[m";
178+
else
179+
return str;
180+
}
181+
182+
std::size_t consolet::width()
183+
{
184+
std::size_t width = 80; // default
185+
186+
if(_is_terminal)
187+
{
188+
#ifdef _WIN32
189+
HANDLE h = GetStdHandle(STD_OUTPUT_HANDLE);
190+
CONSOLE_SCREEN_BUFFER_INFO info;
191+
GetConsoleScreenBufferInfo(h, &info);
192+
width = info.srWindow.Right - info.srWindow.Left + 1;
193+
#else
194+
std::ostringstream width_stream;
195+
run("stty", {"stty", "size"}, "", width_stream, "");
196+
auto stty_output = split_string(width_stream.str(), ' ');
197+
if(
198+
stty_output.size() >= 1 && !stty_output[1].empty() &&
199+
isdigit(stty_output[1][0]))
200+
{
201+
auto width_l = atol(stty_output[1].c_str());
202+
if(width_l >= 10 && width_l <= 400)
203+
width = width_l;
204+
}
205+
#endif
206+
}
207+
208+
return width;
209+
}
210+
211+
consolet::redirectt::redirectt(
212+
std::ostream &__console_out,
213+
std::ostream &__console_err)
214+
{
215+
consolet::init();
216+
old_out = consolet::_out;
217+
old_err = consolet::_err;
218+
old_is_terminal = consolet::_is_terminal;
219+
consolet::_out = &__console_out;
220+
consolet::_err = &__console_err;
221+
consolet::_is_terminal = false;
222+
}
223+
224+
consolet::redirectt::~redirectt()
225+
{
226+
consolet::_out = old_out;
227+
consolet::_err = old_err;
228+
consolet::_is_terminal = old_is_terminal;
229+
}

Diff for: src/util/console.h

+90
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
/*******************************************************************\
2+
3+
Module: Console
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Console
11+
12+
#ifndef CPROVER_CPROVER_CONSOLE_H
13+
#define CPROVER_CPROVER_CONSOLE_H
14+
15+
#include <cstddef>
16+
#include <iosfwd>
17+
18+
class consolet
19+
{
20+
public:
21+
/// Modifiers for console output
22+
static std::ostream &blue(std::ostream &);
23+
static std::ostream &cyan(std::ostream &);
24+
static std::ostream &green(std::ostream &);
25+
static std::ostream &red(std::ostream &);
26+
static std::ostream &yellow(std::ostream &);
27+
static std::ostream &orange(std::ostream &);
28+
29+
static std::ostream &bold(std::ostream &);
30+
static std::ostream &faint(std::ostream &);
31+
static std::ostream &underline(std::ostream &);
32+
33+
static std::ostream &reset(std::ostream &);
34+
35+
/// \return true if the console is a terminal.
36+
static bool is_terminal()
37+
{
38+
init();
39+
return _is_terminal;
40+
}
41+
42+
/// \return true if "Select Graphic Rendition" is used.
43+
static bool use_SGR()
44+
{
45+
init();
46+
return _use_SGR;
47+
}
48+
49+
/// Stream for standard output.
50+
static std::ostream &out()
51+
{
52+
init();
53+
return *_out;
54+
}
55+
56+
/// Stream for error output.
57+
static std::ostream &err()
58+
{
59+
init();
60+
return *_err;
61+
}
62+
63+
/// \return the width of the console in characters
64+
static std::size_t width();
65+
66+
/// Console redirection to a stream.
67+
/// The previous state is restored when this object is destroyed.
68+
class redirectt
69+
{
70+
public:
71+
// __out has some meaning on Windows, therefore using __console_out
72+
redirectt(std::ostream &__console_out, std::ostream &__console_err);
73+
~redirectt();
74+
75+
protected:
76+
std::ostream *old_out = nullptr, *old_err = nullptr;
77+
bool old_is_terminal = false;
78+
};
79+
80+
protected:
81+
static void init();
82+
83+
static bool _is_terminal;
84+
static bool _use_SGR;
85+
static bool _init_done;
86+
static std::ostream *_out;
87+
static std::ostream *_err;
88+
};
89+
90+
#endif // CPROVER_CPROVER_CONSOLE_H

0 commit comments

Comments
 (0)