michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Change operators in format:

Browse source 
f1 + f2 = f1 <> f2
f1 ^ f2 = f1 <> " " <> f2
This commit is contained in:
Soonho Kong 2013-08-02 19:17:29 -07:00
parent bddecd7d9c
commit 5f10d47035
2 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/format.cpp
View file

@ -237,6 +237,10 @@ format operator+(format const & f1, format const & f2) {
return format{f1, f2}; return format{f1, f2};
} }
format operator^(format const & f1, format const & f2) {
return format{f1, format(" "), f2};
}
std::ostream & pretty(std::ostream & out, unsigned w, format const & f) { std::ostream & pretty(std::ostream & out, unsigned w, format const & f) {
sexpr const & b = format::best(w, 0, f.m_value); sexpr const & b = format::best(w, 0, f.m_value);
return layout_list(out, b); return layout_list(out, b);

13
src/util/format.h
View file

@ -177,13 +177,22 @@ public:
friend format bracket(std::string const l, format const & x, std::string const r); friend format bracket(std::string const l, format const & x, std::string const r);
friend format wrap(format const & f1, format const & f2); friend format wrap(format const & f1, format const & f2);
// x + y = x <> y
friend format operator+(format const & f1, format const & f2);
format & operator+=(format const & f) { format & operator+=(format const & f) {
*this = *this + f; *this = *this + f;
return *this; return *this;
} }
// x ^ y = x <> " " <> y
friend format operator^(format const & f1, format const & f2);
format & operator^=(format const & f) {
*this = *this ^ f;
return *this;
}
friend std::ostream & operator<<(std::ostream & out, format const & f); friend std::ostream & operator<<(std::ostream & out, format const & f);
// x <+> y = x <> text " " <> y
friend format operator+(format const & f1, format const & f2);
friend std::ostream & layout(std::ostream & out, sexpr const & s); friend std::ostream & layout(std::ostream & out, sexpr const & s);
friend std::ostream & pretty(std::ostream & out, unsigned w, format const & f); friend std::ostream & pretty(std::ostream & out, unsigned w, format const & f);
}; };