changeset 1637:e374b6b8ab38

Allow .urp libraries to set prefix
author Adam Chlipala <adam@chlipala.net>
date Sat, 17 Dec 2011 13:10:23 -0500 (2011-12-17)
parents 2b312f6d4007
children 3bf727a08db8
files src/compiler.sml src/settings.sig src/settings.sml
diffstat 3 files changed, 18 insertions(+), 2 deletions(-) [+]
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,
--- a/src/settings.sig	Sat Dec 17 12:01:31 2011 -0500
+++ b/src/settings.sig	Sat Dec 17 13:10:23 2011 -0500
@@ -36,6 +36,10 @@
     val setUrlPrefix : string -> unit
     val getUrlPrefix : unit -> string
     val getUrlPrePrefix : unit -> string
+    val getUrlPrefixFull : unit -> string
+    (* The full prefix is the value that was set explicitly, while the "pre"
+     * prefix gets the protocol/host/port part and the unqualified prefix gets
+     * the URI. *)
 
     (* How many seconds should the server wait before assuming a Comet client has left? *)
     val setTimeout : int -> unit
--- a/src/settings.sml	Sat Dec 17 12:01:31 2011 -0500
+++ b/src/settings.sml	Sat Dec 17 13:10:23 2011 -0500
@@ -27,12 +27,14 @@
 
 structure Settings :> SETTINGS = struct
 
+val urlPrefixFull = ref "/"
 val urlPrefix = ref "/"
 val urlPrePrefix = ref ""
 val timeout = ref 0
 val headers = ref ([] : string list)
 val scripts = ref ([] : string list)
 
+fun getUrlPrefixFull () = !urlPrefixFull
 fun getUrlPrefix () = !urlPrefix
 fun getUrlPrePrefix () = !urlPrePrefix
 fun setUrlPrefix p =
@@ -62,6 +64,7 @@
             else
                 ("", prefix)
     in
+        urlPrefixFull := p;
         urlPrePrefix := prepre;
         urlPrefix := prefix
     end