Merge branch 'upstream' into dfsg_clean20161022+dfsg

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