summaryrefslogtreecommitdiff
path: root/src/fileio.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/fileio.sml')
-rw-r--r--src/fileio.sml39
1 files changed, 39 insertions, 0 deletions
diff --git a/src/fileio.sml b/src/fileio.sml
new file mode 100644
index 00000000..cab9d8a3
--- /dev/null
+++ b/src/fileio.sml
@@ -0,0 +1,39 @@
+structure FileIO :> FILE_IO = struct
+
+val mostRecentModTimeRef = ref (Time.zeroTime)
+
+fun checkFileModTime fname =
+ let
+ val mtime = OS.FileSys.modTime fname
+ val mostRecentMod = !mostRecentModTimeRef
+ val resetTime = Globals.getResetTime ()
+ fun lessThan (a, b) = LargeInt.compare (Time.toSeconds a, Time.toSeconds b) = LESS
+ infix lessThan
+ in
+ if mostRecentMod lessThan mtime andalso mtime lessThan resetTime
+ then mostRecentModTimeRef := mtime
+ else ()
+ end
+
+fun mostRecentModTime () =
+ if Time.compare (!mostRecentModTimeRef, Time.zeroTime) = EQUAL
+ then Globals.getResetTime ()
+ else !mostRecentModTimeRef
+
+fun txtOpenIn fname =
+ let
+ val inf = TextIO.openIn fname
+ val () = checkFileModTime fname
+ in
+ inf
+ end
+
+fun binOpenIn fname =
+ let
+ val inf = BinIO.openIn fname
+ val () = checkFileModTime fname
+ in
+ inf
+ end
+
+end