@@ -60,10 +60,10 @@ data FileIO : Effect where
60 ||| Only files that are open for reading can be read.
60 ||| Only files that are open for reading can be read.
61 ReadLine : {OpenFile Read} FileIO String
61 ReadLine : {OpenFile Read} FileIO String
63− ||| Write a line to a file.
63+ ||| Write a string to a file.
65 ||| Only file that are open for writing can be written to.
65 ||| Only file that are open for writing can be written to.
66− WriteLine : String -> {OpenFile Write} FileIO ()
66+ WriteString : String -> {OpenFile Write} FileIO ()
68 ||| End of file?
68 ||| End of file?
@@ -82,8 +82,8 @@ instance Handler FileIO IO where
83 handle (FH h) ReadLine k = do str <- fread h
83 handle (FH h) ReadLine k = do str <- fread h
84 k str (FH h)
84 k str (FH h)
85− handle (FH h) (WriteLine str) k = do fwrite h str
85+ handle (FH h) (WriteString str) k = do fwrite h str
86− k () (FH h)
86+ k () (FH h)
87 handle (FH h) EOF k = do e <- feof h
87 handle (FH h) EOF k = do e <- feof h
88 k e (FH h)
88 k e (FH h)
@@ -117,9 +117,13 @@ close = call $ Close
117readLine : { [FILE_IO (OpenFile Read)] } Eff String
117readLine : { [FILE_IO (OpenFile Read)] } Eff String
118readLine = call $ ReadLine
118readLine = call $ ReadLine
120+||| Write a string to a file.
121+writeString : String -> { [FILE_IO (OpenFile Write)] } Eff ()
122+writeString str = call $ WriteString str
120||| Write a line to a file.
124||| Write a line to a file.
121writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()
125writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()
122−writeLine str = call $ WriteLine str
126+writeLine str = call $ WriteString (str ++ "\n")
124||| End of file?
128||| End of file?
125eof : { [FILE_IO (OpenFile Read)] } Eff Bool
129eof : { [FILE_IO (OpenFile Read)] } Eff Bool