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
|
\DOC strings_of_file
\TYPE {strings_of_file : string -> string list}
\SYNOPSIS
Read file and convert content into a list of strings.
\DESCRIBE
When given a filename, the function {strings_of_file} attempts to open the file
for input, and if this is successful reads and closes it, returning a list of
strings corresponding to the lines in the file.
\FAILURE
Fails if the file cannot be opened (e.g. it does not exist, or the permissions
are wrong).
\EXAMPLE
If the file {/tmp/greeting} contains the text
{
Hello world
Goodbye world
}
\noindent then
{
# strings_of_file "/tmp/greeting";;
val it : string list = ["Hello world"; "Goodbye world"]
}
\SEEALSO
file_of_string, string_of_file.
\ENDDOC
|
