Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.IO.UTF8

Description

Text IO using the UTF8 character encoding.

Synopsis

- data ReadException
- readTextFile :: FilePath -> IO Text
- readFile :: FilePath -> IO String
- writeFile :: FilePath -> String -> IO ()
- writeTextToFile :: FilePath -> Text -> IO ()

# Documentation

data ReadException Source #

A kind of exception that can be thrown by `readTextFile` and `readFile`.

#### Instances

Instances details

Exception ReadException Source # |
Instance details Defined in Agda.Utils.IO.UTF8 Methods toException :: ReadException -> SomeException Source # fromException :: SomeException -> Maybe ReadException Source # displayException :: ReadException -> String Source # backtraceDesired :: ReadException -> Bool Source #
Show ReadException Source # |
Instance details Defined in Agda.Utils.IO.UTF8 Methods showsPrec :: Int -> ReadException -> ShowS Source # show :: ReadException -> String Source # showList :: [ReadException] -> ShowS Source #

readTextFile :: FilePath -> IO Text Source #

Reads a UTF8-encoded text file and converts many character sequences which may be interpreted as line or paragraph separators into 'n'.

If the file cannot be decoded, then a `ReadException` is raised.

readFile :: FilePath -> IO String Source #

Reads a UTF8-encoded text file and converts many character sequences which may be interpreted as line or paragraph separators into 'n'.

If the file cannot be decoded, then a `ReadException` is raised.

writeFile :: FilePath -> String -> IO () Source #

Writes a UTF8-encoded text file. The native convention for line endings is used.

writeTextToFile :: FilePath -> Text -> IO () Source #

Writes a UTF8-encoded text file. The native convention for line endings is used.