idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-03 00:36:37 +03:00
Code Issues Projects Releases Wiki Activity

withFile & writeFile cleanup (#1085)

Browse Source
This commit is contained in:
Mathew Polzin 2021-02-18 09:51:45 -08:00 committed by GitHub
parent 26464357c1
commit d5d0b64b4a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
libs/base/System/File.idr
View File

@ -314,14 +314,14 @@ export
withFile : HasIO io => (filename : String) ->
Mode ->
(onError : FileError -> io a) ->
(onOpen : File -> io b) ->
(onOpen : File -> io (Either a b)) ->
io (Either a b)
withFile filename mode onError onOpen =
do Right h <- openFile filename mode
| Left err => Left <$> onError err
res <- onOpen h
closeFile h
pure $ Right res
pure res
try : Monad m => m (Either FileError a) -> (a -> m (Either FileError b)) -> m (Either FileError b)
try a f = a >>= either (pure . Left) f
@ -361,8 +361,8 @@ readLinesOnto acc offset (More fuel) h
export
readFilePage : HasIO io => (offset : Nat) -> (until : Fuel) -> String -> io (Either FileError (Bool, List String))
readFilePage offset fuel file
= join <$> (withFile file Read pure $
readLinesOnto [] offset fuel)
= withFile file Read pure $
readLinesOnto [] offset fuel
export
partial
@ -374,14 +374,9 @@ export
writeFile : HasIO io =>
(filepath : String) -> (contents : String) ->
io (Either FileError ())
writeFile fn contents = do
Right h <- openFile fn WriteTruncate
| Left err => pure (Left err)
Right () <- fPutStr h contents
| Left err => do closeFile h
pure (Left err)
closeFile h
pure (Right ())
writeFile file contents
= withFile file WriteTruncate pure $
(flip fPutStr contents)
namespace FileMode
public export