on master help sign in
Fix deprecation warnings for File Writing.
commit87f1da9b6ef2c2e14feefcfee893f1ac3792140c authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateMon 8 Feb 2016, 15:15 (11 years ago) parent50f4c82
2 files changed+6−6
libs/effects/Effect/File.idr+4−4 libs/prelude/Prelude/File.idr+2−2
libs/effects/Effect/File.idr+4−4
@@ -64,7 +64,7 @@ data FileIO : Effect where
6464 ||| Write a string to a file.
6565 |||
6666 ||| Only file that are open for writing can be written to.
67− WriteString : String -> sig FileIO () (OpenFile Write)
67+ WriteString : String -> sig FileIO () (OpenFile WriteTruncate)
6868
6969 ||| End of file?
7070 |||
@@ -138,11 +138,11 @@ readLine : Eff String [FILE_IO (OpenFile Read)]
138138readLine = call $ ReadLine
139139
140140||| Write a string to a file.
141−writeString : String -> Eff () [FILE_IO (OpenFile Write)]
141+writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
142142writeString str = call $ WriteString str
143143
144144||| Write a line to a file.
145−writeLine : String -> Eff () [FILE_IO (OpenFile Write)]
145+writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
146146writeLine str = call $ WriteString (str ++ "\n")
147147
148148||| End of file?
@@ -176,7 +176,7 @@ writeFile : (errFunc : String -> e)
176176 -> (content : String)
177177 -> Eff (Either e ()) [FILE_IO ()]
178178writeFile errFunc fname content = do
179− case !(open fname Write) of
179+ case !(open fname WriteTruncate) of
180180 True => do
181181 writeString content
182182 close
libs/prelude/Prelude/File.idr+2−2
@@ -255,7 +255,7 @@ export
255255writeFile : (filepath : String) -> (contents : String) ->
256256 IO (Either FileError ())
257257writeFile fn contents = do
258− Right h <- openFile fn Write | Left err => return (Left err)
259− Right () <- fPutStr h contents | Left err => return (Left err)
258+ Right h <- openFile fn WriteTruncate | Left err => return (Left err)
259+ Right () <- fPutStr h contents | Left err => return (Left err)
260260 closeFile h
261261 return (Right ())