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

Fix bug in sexpr operator <<.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-07 21:04:41 -07:00
parent 0f48f73e14
commit bede62e2f7
2 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/tests/util/sexpr/sexpr.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <sstream>
#include "sexpr.h"
#include "sexpr_funcs.h"
#include "mpq.h"
@ -154,6 +155,12 @@ static void tst5() {
== 987654321);
}
static void tst6() {
std::ostringstream s;
sexpr foo("str with \"quote\"");
s << foo;
lean_assert(s.str() == "\"str with \\\"quote\\\"\"");
}
int main() {
continue_on_violation(true);
@ -162,5 +169,6 @@ int main() {
tst3();
tst4();
tst5();
tst6();
return has_violations() ? 1 : 0;
}

3
src/util/sexpr/sexpr.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "name.h"
#include "mpz.h"
#include "mpq.h"
#include "escaped.h"
namespace lean {
/** \brief Base class used to represent S-expression cells. */
@ -213,7 +214,7 @@ int cmp(sexpr const & a, sexpr const & b) {
std::ostream & operator<<(std::ostream & out, sexpr const & s) {
switch (s.kind()) {
case sexpr_kind::NIL: out << "nil"; break;
case sexpr_kind::STRING: out << "\"" << to_string(s) << "\""; break;
case sexpr_kind::STRING: out << "\"" << escaped(to_string(s).c_str()) << "\""; break;
case sexpr_kind::INT: out << to_int(s); break;
case sexpr_kind::DOUBLE: out << to_double(s); break;
case sexpr_kind::NAME: out << to_name(s); break;