comparison src/settings.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 deeeb036c8ed
children ac141fbb313a
comparison
equal deleted inserted replaced
1636:2b312f6d4007 1637:e374b6b8ab38
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 structure Settings :> SETTINGS = struct 28 structure Settings :> SETTINGS = struct
29 29
30 val urlPrefixFull = ref "/"
30 val urlPrefix = ref "/" 31 val urlPrefix = ref "/"
31 val urlPrePrefix = ref "" 32 val urlPrePrefix = ref ""
32 val timeout = ref 0 33 val timeout = ref 0
33 val headers = ref ([] : string list) 34 val headers = ref ([] : string list)
34 val scripts = ref ([] : string list) 35 val scripts = ref ([] : string list)
35 36
37 fun getUrlPrefixFull () = !urlPrefixFull
36 fun getUrlPrefix () = !urlPrefix 38 fun getUrlPrefix () = !urlPrefix
37 fun getUrlPrePrefix () = !urlPrePrefix 39 fun getUrlPrePrefix () = !urlPrePrefix
38 fun setUrlPrefix p = 40 fun setUrlPrefix p =
39 let 41 let
40 val prefix = if p = "" then 42 val prefix = if p = "" then
60 else if String.isPrefix "https://" prefix then 62 else if String.isPrefix "https://" prefix then
61 findPrefix 8 63 findPrefix 8
62 else 64 else
63 ("", prefix) 65 ("", prefix)
64 in 66 in
67 urlPrefixFull := p;
65 urlPrePrefix := prepre; 68 urlPrePrefix := prepre;
66 urlPrefix := prefix 69 urlPrefix := prefix
67 end 70 end
68 71
69 fun getTimeout () = !timeout 72 fun getTimeout () = !timeout