@@ -27,7 +27,7 @@ data File : Type where
2727||| An error from a file operation
2828-- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
2929-- the values correspond!
30−
30+
3131data FileError = GenericFileError Int -- errno
3232 | FileReadError
3333 | FileWriteError
@@ -102,10 +102,6 @@ validFile (FHandle h) = do x <- nullPtr h
102102||| Modes for opening files
103103data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend
104104
105−Write : Mode
106−Write = WriteTruncate
107−%deprecate Write "Please use WriteTruncate instead."
108−
109105modeStr : Mode -> String
110106modeStr Read = "r"
111107modeStr WriteTruncate = "w"
@@ -142,12 +138,12 @@ do_getFileSize h = foreign FFI_C "fileSize" (Ptr -> IO Int) h
142138
143139||| Return the size of a File
144140||| Returns an error if the File is not an ordinary file (e.g. a directory)
145−||| Also note that this currently returns an Int, which may overflow if the
141+||| Also note that this currently returns an Int, which may overflow if the
146142||| file is very big
147143export
148144fileSize : File -> IO (Either FileError Int)
149145fileSize (FHandle h) = do s <- do_getFileSize h
150− if (s < 0)
146+ if (s < 0)
151147 then do err <- getFileError
152148 pure (Left err)
153149 else pure (Right s)
@@ -187,21 +183,16 @@ export
187183pclose : File -> IO ()
188184pclose (FHandle h) = foreign FFI_C "pclose" (Ptr -> IO ()) h
189185
190−-- mkForeign (FFun "idris_readStr" [FPtr, FPtr] (FAny String))
191−-- prim__vm h
192−
193−export
194−fread : File -> IO (Either FileError String)
195−fread (FHandle h) = do str <- do_fread h
196− if !(ferror (FHandle h))
197− then pure (Left FileReadError)
198− else pure (Right str)
199186
200187||| Read a line from a file
201188||| @h a file handle which must be open for reading
202189export
203190fGetLine : (h : File) -> IO (Either FileError String)
204−fGetLine = fread
191+fGetLine (FHandle h) = do
192+ str <- do_fread h
193+ if !(ferror (FHandle h))
194+ then pure (Left FileReadError)
195+ else pure (Right str)
205196
206197||| Read up to a number of characters from a file
207198||| @h a file handle which must be open for reading
@@ -212,7 +203,6 @@ fGetChars (FHandle h) len = do str <- do_freadChars h len
212203 then pure (Left FileReadError)
213204 else pure (Right str)
214205
215−%deprecate fread "Use fGetLine instead"
216206
217207private
218208do_fwrite : Ptr -> String -> IO (Either FileError ())
@@ -225,10 +215,6 @@ do_fwrite h s = do res <- prim_fwrite h s
225215 pure (Left err)
226216 else pure (Right ())
227217
228−export
229−fwrite : File -> String -> IO (Either FileError ())
230−fwrite (FHandle h) s = do_fwrite h s
231−
232218||| Write a line to a file
233219||| @h a file handle which must be open for writing
234220||| @str the line to write to the file
@@ -240,8 +226,6 @@ export
240226fPutStrLn : File -> String -> IO (Either FileError ())
241227fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")
242228
243−%deprecate fwrite "Use fPutStr instead"
244−
245229private
246230do_feof : Ptr -> IO Int
247231do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
@@ -252,13 +236,6 @@ fEOF : File -> IO Bool
252236fEOF (FHandle h) = do eof <- do_feof h
253237 pure (not (eof == 0))
254238
255−||| Check if a file handle has reached the end
256−export
257−feof : File -> IO Bool
258−feof = fEOF
259−
260−%deprecate feof "Use fEOF instead"
261−
262239export
263240fpoll : File -> IO Bool
264241fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h