/usr/share/hol88-2.02.19940316/help/ENTRIES/write.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 36 37 38 39 40 41 42 | \DOC write
\TYPE {write : ((string # string) -> void)}
\SYNOPSIS
Writes characters to a file.
\KEYWORDS
file.
\DESCRIBE
The call {write(port,`characters`)}, where {characters} is a string of
characters to write, and {port} is a string describing a port (a port is the
standard ML file descriptor, normally obtained from a call to {openw} or
{append_openw}), will write the given characters to the file corresponding to
the port.
\FAILURE
May fail or hang in system-dependent ways when given an invalid port
descriptor.
\EXAMPLE
The following assumes that HOL is being run under Unix. It will overwrite any
existing file {test-file} in the current directory. Notice that the actual
string returned by {openw} may vary on other systems.
{
#let port = openw `test-file`;;
port = `%test-file` : string
#write(port,`Hello world`);;
() : void
#close port;;
() : void
#system `cat test-file`;;
Hello world0 : int
}
\SEEALSO
append_openw, close, openi, openw, read, tty_read, tty_write.
\ENDDOC
|