File

This structure provides access to the UNIX filehandling interface.

Signature of File

List of Import References :
See BOOL
See Char
See Com
See DENOTATION
See Int
See Nat
See Option
See Seq
See String
See Void

SIGNATURE File

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

IMPORT  Char            ONLY char
        Void            ONLY void
        Nat             ONLY nat
        Int             ONLY int
        String          ONLY string
        Com[bool]       ONLY com
        Com[char]       ONLY com
        Com[void]       ONLY com
        Com[string]     ONLY com
        Com[nat]        ONLY com
        Com[file]       ONLY com
       Com[seq[string]] ONLY com
       Seq[string] ONLY seq

SORT file

Standard Files

FUN stdIn stdOut stdErr : file

Opening and Closing Files

open(fn,kind) opens file named fn, kind indicates the allowed operations (similar to fopen(3)):

`"r"'

open for reading

`"w"'

open for writing

`"a"'

open for writing, append, if file exists

`"...+"'

open for reading and writing

`"...b"'

binary file

FUN open        : denotation ** denotation -> com[file]

reopen(fn, kind, file) reopens file under name fn and kind.

FUN reopen      : denotation ** denotation ** file -> com[void]

Close given file

FUN close       : file -> com[void]

Positioning in a File

True, iff file pointer is at end? (2)

FUN eof?        : file -> com[bool]

Return current position in file

FUN tell        : file -> com[nat]

Seek to specified position.

FUN seek        : file ** int ** seekMode -> com[void]
TYPE seekMode == fromStart fromCurrent fromEnd

Rewind file to the beginning.

FUN rewind      : file -> com[void]

Reading

NOTE: Processing files character-by-character will be slow because of the overhead involved by command evaluation.

Read next character-by-character.

FUN read        : file -> com[char]

Unread last read character.

FUN unread      : file ** char -> com[void]

Read at most number characters. Use max'Nat to read the whole file into a string.

FUN read        : file ** nat -> com[string]

Read string while predicate holds or until EOF occurs.

FUN read        : file ** (char -> bool) -> com[string]

Read next line or until EOF. Result will not contain the newline.

FUN readLine    : file -> com[string]

Read following lines until EOF.

FUN readLines      : file -> com[seq[string]]

Writing

NOTE: Processing files character-by-character will be slow because of the overhead involved by command evaluation.

Write a character, a denotation, a string to file.

FUN write       : file ** char -> com[void]
FUN write       : file ** denotation -> com[void]
FUN write       : file ** string -> com[void]

Write a denotation or a string, followed by a newline.

FUN writeLine   : file ** denotation -> com[void]
FUN writeLine   : file ** string -> com[void]

Write lines to file

FUN writeLines  : file ** seq[string] -> com[void]

Miscellaneous

flush(f) writes buffered data, if f is opened for writing. Ffect is undefined, if f is opened for reading!

FUN flush       : file -> com[void]

True, if last operation failed?

FUN error?      : file -> com[bool]

Size of file

FUN size        : file -> com[nat]

-- ... more functions to come ...

next node: ProcessComInterrupt,
prev node: UnixFailures,
up to node: Subsystem Unix