diff src/cjr_print.sml @ 1285:514be09d5018

Better UTF-8 escaping for JavaScript and SQL literals
author Adam Chlipala <adam@chlipala.net>
date Tue, 10 Aug 2010 15:55:43 -0400
parents be2ef50780ed
children acabf3935060
line wrap: on
line diff
--- a/src/cjr_print.sml	Tue Aug 10 14:52:33 2010 -0400
+++ b/src/cjr_print.sml	Tue Aug 10 15:55:43 2010 -0400
@@ -2128,7 +2128,7 @@
       | DPreparedStatements _ => box []
 
       | DJavaScript s => box [string "static char jslib[] = \"",
-                              string (String.toString s),
+                              string (String.toCString s),
                               string "\";"]
       | DCookie s => box [string "/*",
                           space,
@@ -2585,7 +2585,7 @@
                             prefix ^ s
             in
                 box [string "if (!strncmp(request, \"",
-                     string (String.toString s),
+                     string (String.toCString s),
                      string "\", ",
                      string (Int.toString (size s)),
                      string ") && (request[",
@@ -2761,10 +2761,10 @@
                           box [string "if (!str",
                                case #kind rule of
                                    Settings.Exact => box [string "cmp(s, \"",
-                                                          string (String.toString (#pattern rule)),
+                                                          string (String.toCString (#pattern rule)),
                                                           string "\"))"]
                                  | Settings.Prefix => box [string "ncmp(s, \"",
-                                                           string (String.toString (#pattern rule)),
+                                                           string (String.toCString (#pattern rule)),
                                                            string "\", ",
                                                            string (Int.toString (size (#pattern rule))),
                                                            string "))"],