/usr/share/hol88-2.02.19940316/help/ENTRIES/openi.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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
|