diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2015-12-05 12:04:06 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2015-12-05 12:04:06 -0500 |
| commit | bad7adde120773d46af83ab972967f26823e37b4 (patch) | |
| tree | a1e8aac4d22273e103ddf675ee88f19b3fee2e0a /src/settings.sml | |
| parent | 4635acd2d4e4404b2b1a89909cd765ac310d62c5 (diff) | |
New .urp directive: jsFile
Diffstat (limited to 'src/settings.sml')
| -rw-r--r-- | src/settings.sml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/settings.sml b/src/settings.sml index 8300d621..650122ca 100644 --- a/src/settings.sml +++ b/src/settings.sml @@ -903,6 +903,25 @@ fun addFile {Uri, LoadFromFilename} = fun listFiles () = map #2 (SM.listItems (!files)) +val jsFiles = ref (SM.empty : {Filename : string, Content : string} SM.map) + +fun addJsFile LoadFromFilename = + let + val path = OS.Path.concat (!filePath, LoadFromFilename) + val inf = TextIO.openIn path + in + jsFiles := SM.insert (!jsFiles, + path, + {Filename = LoadFromFilename, + Content = TextIO.inputAll inf}); + TextIO.closeIn inf + end handle IO.Io _ => + ErrorMsg.error ("Error loading file " ^ LoadFromFilename) + | OS.SysErr (s, _) => + ErrorMsg.error ("Error loading file " ^ LoadFromFilename ^ " (" ^ s ^ ")") + +fun listJsFiles () = SM.listItems (!jsFiles) + fun reset () = (urlPrefixFull := "/"; urlPrefix := "/"; @@ -945,6 +964,7 @@ fun reset () = noMimeFile := false; mimeTypes := NONE; files := SM.empty; + jsFiles := SM.empty; filePath := ".") end |