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

Fix sexpr_text_length function to handle quotation in string

Browse source
This commit is contained in:
Soonho Kong 2013-08-08 12:23:42 -07:00
parent 9516d9f88f
commit 635407ca4a
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/util/format.h
View file

@ -82,7 +82,12 @@ private:
static inline size_t const sexpr_text_length(sexpr const & s) {
lean_assert(sexpr_kind(s) == format_kind::TEXT);
std::stringstream ss;
ss << cdr(s);
sexpr const & content = cdr(s);
if(is_string(content)) {
ss << to_string(content);
} else {
ss << content;
}
return ss.str().length();
}
static inline sexpr sexpr_text(std::string const & s) {