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
43
|
\DOC set_search_path
\TYPE {set_search_path : (string list -> void)}
\SYNOPSIS
Sets the internal search path used by HOL to find files.
\DESCRIBE
When applied to a list of strings {l}, each of which represents a directory
pathname, {set_search_path} sets the internal search path used when HOL makes
access to files on disk to the list {l}. Although the search path can be set to
an arbitrary list of strings, each string in the search path is normally
expected to be either empty ({``}) or a pathname with `{/}' as its final
character. When HOL looks for a file, the directories in the search path are
searched in the order in which they occur in the list supplied to
{set_search_path}.
\FAILURE
Never fails.
\EXAMPLE
A typical search path is the following:
{
#search_path();;
[``; `~/`; `/usr/lib/hol/theories/`] : string list
}
\noindent With this search path, HOL first looks for a file in the current
working directory (the pathname represented by {``}), then in the user`s home
directory {`~/`}, and finally in the directory {`/usr/lib/hol/theories/`} (the
directory containing HOL`s built-in theories).
One might augment this search path by doing:
{
#set_search_path(`/foo/bar/` . search_path());;
() : void
}
\noindent so that the directory {/foo/bar/} is also searched, and searched
first, when HOL tries to find a file.
\SEEALSO
help_search_path, install, search_path, set_help_search_path.
\ENDDOC
|
