File: openi.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (25 lines) | stat: -rw-r--r-- 562 bytes parent folder | download | duplicates (11)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
\DOC openi

\TYPE {openi : (string -> string)}

\SYNOPSIS
Opens a named port for input from a named file.

\KEYWORDS
file.

\DESCRIBE
Given a string argument {`foo`}, {openi} returns a string (a port identifier)
that can be used by the function {read} to read characters from the file {foo}.
The port identifier is also used as an argument to the function {close};
{close} terminates input.

\FAILURE
Fails if the file cannot be found with the current search path or if
read permission on the named file
is disabled.

\SEEALSO
close, openw, read, write

\ENDDOC