on master help sign in
Added Prelude.File.writeFile
92bdae5Edwin Brady
libs/prelude/Prelude/File.idr+8−2
@@ -40,7 +40,6 @@ getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
40 return err
40 return err
41
41
42instance Show FileError where
42instance Show FileError where
43− show Success = "Success"
44 show FileNotFound = "File Not Found"
43 show FileNotFound = "File Not Found"
45 show PermissionDenied = "Permission Denied"
44 show PermissionDenied = "Permission Denied"
46 show (GenericFileError errno) = strError errno
45 show (GenericFileError errno) = strError errno
@@ -184,4 +183,11 @@ readFile fn = do Right h <- openFile fn Read
184 readFile' h (contents ++ l)
183 readFile' h (contents ++ l)
185 else return (Right contents)
184 else return (Right contents)
186
185
187−
186+||| Write a string to a file
187+writeFile : (filepath : String) -> (contents : String) ->
188+ IO (Either FileError ())
189+writeFile fn contents = do
190+ Right h <- openFile fn Write | Left err => return (Left err)
191+ Right () <- fwrite h contents | Left err => return (Left err)
192+ closeFile h
193+ return (Right ())