/usr/share/hol88-2.02.19940316/help/ENTRIES/openw.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 26 27 28 29 30 31 32 33 34 35 | \DOC openw
\TYPE {openw : (string -> string)}
\SYNOPSIS
Opens a port for writing to a named file.
\KEYWORDS
file.
\DESCRIBE
Given a string argument {`foo`}, {openw} creates a new file {foo}
(overwriting an existing file with the same name) and returns a string
(a port identifier) that can be used by {write} to write characters to the
file. The port identifier is also used by {close} to close the file.
\EXAMPLE
{
#let port = openw `foo`;;
port = `%foo` : string
#write (port, `contents of file foo\L`);;
() : void
#close port;;
() : void
#system `cat foo`;;
contents of file foo
0 : int
}
\SEEALSO
close, openi, read, write
\ENDDOC
|