@@ -60,10 +60,10 @@ data FileIO : Effect where
6060 ||| Only files that are open for reading can be read.
6161 ReadLine : {OpenFile Read} FileIO String
6262
63− ||| Write a line to a file.
63+ ||| Write a string to a file.
6464 |||
6565 ||| Only file that are open for writing can be written to.
66− WriteLine : String -> {OpenFile Write} FileIO ()
66+ WriteString : String -> {OpenFile Write} FileIO ()
6767
6868 ||| End of file?
6969 |||
@@ -82,8 +82,8 @@ instance Handler FileIO IO where
8282 k () ()
8383 handle (FH h) ReadLine k = do str <- fread h
8484 k str (FH h)
85− handle (FH h) (WriteLine str) k = do fwrite h str
86− k () (FH h)
85+ handle (FH h) (WriteString str) k = do fwrite h str
86+ k () (FH h)
8787 handle (FH h) EOF k = do e <- feof h
8888 k e (FH h)
8989
@@ -117,9 +117,13 @@ close = call $ Close
117117readLine : { [FILE_IO (OpenFile Read)] } Eff String
118118readLine = call $ ReadLine
119119
120+||| Write a string to a file.
121+writeString : String -> { [FILE_IO (OpenFile Write)] } Eff ()
122+writeString str = call $ WriteString str
123+
120124||| Write a line to a file.
121125writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()
122−writeLine str = call $ WriteLine str
126+writeLine str = call $ WriteString (str ++ "\n")
123127
124128||| End of file?
125129eof : { [FILE_IO (OpenFile Read)] } Eff Bool