From 635407ca4a994604acd77ed8f252dcf9ea0ab662 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Thu, 8 Aug 2013 12:23:42 -0700
Subject: [PATCH] Fix sexpr_text_length function to handle quotation in string

---
 src/util/format.h | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/util/format.h b/src/util/format.h
index 176b35662..ebbdabf45 100644
--- a/src/util/format.h
+++ b/src/util/format.h
@@ -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) {