comparison src/settings.sml @ 2197:6eae499c56cb

New .urp directive: jsFile
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Dec 2015 12:04:06 -0500
parents fb113569519e
children 6fb9232ade99
comparison
equal deleted inserted replaced
2196:100352dbae36 2197:6eae499c56cb
901 | OS.SysErr (s, _) => 901 | OS.SysErr (s, _) =>
902 ErrorMsg.error ("Error loading file " ^ LoadFromFilename ^ " (" ^ s ^ ")") 902 ErrorMsg.error ("Error loading file " ^ LoadFromFilename ^ " (" ^ s ^ ")")
903 903
904 fun listFiles () = map #2 (SM.listItems (!files)) 904 fun listFiles () = map #2 (SM.listItems (!files))
905 905
906 val jsFiles = ref (SM.empty : {Filename : string, Content : string} SM.map)
907
908 fun addJsFile LoadFromFilename =
909 let
910 val path = OS.Path.concat (!filePath, LoadFromFilename)
911 val inf = TextIO.openIn path
912 in
913 jsFiles := SM.insert (!jsFiles,
914 path,
915 {Filename = LoadFromFilename,
916 Content = TextIO.inputAll inf});
917 TextIO.closeIn inf
918 end handle IO.Io _ =>
919 ErrorMsg.error ("Error loading file " ^ LoadFromFilename)
920 | OS.SysErr (s, _) =>
921 ErrorMsg.error ("Error loading file " ^ LoadFromFilename ^ " (" ^ s ^ ")")
922
923 fun listJsFiles () = SM.listItems (!jsFiles)
924
906 fun reset () = 925 fun reset () =
907 (urlPrefixFull := "/"; 926 (urlPrefixFull := "/";
908 urlPrefix := "/"; 927 urlPrefix := "/";
909 urlPrePrefix := ""; 928 urlPrePrefix := "";
910 timeout := 0; 929 timeout := 0;
943 html5 := false; 962 html5 := false;
944 less := false; 963 less := false;
945 noMimeFile := false; 964 noMimeFile := false;
946 mimeTypes := NONE; 965 mimeTypes := NONE;
947 files := SM.empty; 966 files := SM.empty;
967 jsFiles := SM.empty;
948 filePath := ".") 968 filePath := ".")
949 969
950 end 970 end