diff src/cjr_print.sml @ 1111:e1d738870086

JavaScript urlification; more lenient export pattern in Corify; only include scripts in pages that use JavaScript
author Adam Chlipala <adamc@hcoop.net>
date Sat, 02 Jan 2010 14:54:15 -0500
parents 7fc4e0087e50
children 7a31e0cf25e9
line wrap: on
line diff
--- a/src/cjr_print.sml	Sat Jan 02 13:31:59 2010 -0500
+++ b/src/cjr_print.sml	Sat Jan 02 14:54:15 2010 -0500
@@ -2591,15 +2591,19 @@
                                         val scripts =
                                             case side of
                                                 ServerOnly => ""
-                                              | _ => "<script src=\\\""
-                                                     ^ OS.Path.joinDirFile {dir = Settings.getUrlPrefix (),
-                                                                            file = "app.js"}
-                                                     ^ "\\\"></script>\\n"
-
-                                        val scripts = foldl (fn (x, scripts) =>
-                                                                scripts
-                                                                ^ "<script src=\\\"" ^ x ^ "\\\"></script>\\n")
-                                                      scripts (Settings.getScripts ())
+                                              | _ =>
+                                                let
+                                                    val scripts =
+                                                        "<script src=\\\""
+                                                        ^ OS.Path.joinDirFile {dir = Settings.getUrlPrefix (),
+                                                                               file = "app.js"}
+                                                        ^ "\\\"></script>\\n"
+                                                in
+                                                    foldl (fn (x, scripts) =>
+                                                              scripts
+                                                              ^ "<script src=\\\"" ^ x ^ "\\\"></script>\\n")
+                                                          scripts (Settings.getScripts ())
+                                                end
                                     in
                                         string scripts
                                     end,