diff src/compiler.sml @ 1637:e374b6b8ab38

Allow .urp libraries to set prefix
author Adam Chlipala <adam@chlipala.net>
date Sat, 17 Dec 2011 13:10:23 -0500
parents 438561303d02
children 8de2ea0a0701
line wrap: on
line diff
--- a/src/compiler.sml	Sat Dec 17 12:01:31 2011 -0500
+++ b/src/compiler.sml	Sat Dec 17 13:10:23 2011 -0500
@@ -500,7 +500,7 @@
                           | OnlyComment => readSources acc
                           | EndOfFile => rev acc
 
-                    val prefix = ref (case Settings.getUrlPrefix () of "/" => NONE | s => SOME s)
+                    val prefix = ref (case Settings.getUrlPrefixFull () of "/" => NONE | s => SOME s)
                     val database = ref (Settings.getDbstring ())
                     val exe = ref (Settings.getExe ())
                     val sql = ref (Settings.getSql ())
@@ -580,7 +580,16 @@
                                                         x))
 
                             fun merge (old : job, new : job) = {
-                                prefix = #prefix old,
+                                prefix = case #prefix old of
+                                             "/" => #prefix new
+                                           | pold => case #prefix new of
+                                                         "/" => pold
+                                                       | pnew => (if pold = pnew then
+                                                                      ()
+                                                                  else
+                                                                      ErrorMsg.error ("Multiple prefix values that don't agree: "
+                                                                                      ^ pold ^ ", " ^ pnew);
+                                                                  pold),
                                 database = mergeO (fn (old, _) => old) (#database old, #database new),
                                 exe = #exe old,
                                 sql = #sql old,