blob: 72e72f6d340e4ea93b0042bc393a239db811e729 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
structure FileIO :> FILE_IO = struct
val mostRecentModTimeRef = ref (Time.zeroTime)
fun checkFileModTime fname =
let val mtime = OS.FileSys.modTime fname in
if Time.compare (mtime, !mostRecentModTimeRef) = GREATER andalso
Time.compare (mtime, Globals.getResetTime ()) = LESS
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
|
