/usr/share/hol88-2.02.19940316/help/ENTRIES/autoload.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 43 44 45 46 47 48 49 50 51 52 53 54 55 | \DOC autoload
\TYPE {autoload : ((string # string # string list) -> void)}
\SYNOPSIS
Sets up a general autoloading action.
\DESCRIBE
After a call {autoload(`name`,`f`,[`arg1`;...;`argn`])}, a subsequent
occurrence of {name} in an ML phrase will cause the ML expression
{f [`arg1`;...;`argn`]} to be evaluated before any of the toplevel phrase
containing {name} is evaluated. Notice that {f} is interpreted as a single
identifier denoting a function, whereas the various arguments are string
literals.
\FAILURE
Never fails (obviously failure may occur when the action is actually performed;
the ML phrase could be nonsense).
\EXAMPLE
The following is a simple example:
{
#let action = tty_write o hd;;
action = - : (string list -> void)
#autoload(`key1`,`action`,[`Hello John!`]);;
() : void
#let key1 = 1;;
Hello John!() : void
key1 = 1 : int
}
\COMMENTS
There is no obligation to use the argument list; an alternative to achieve the
same as the above is:
{
#let action (l:(string)list) = tty_write `Hello John!`;;
action = - : (string list -> void)
#autoload(`key2`,`action`,[]);;
() : void
#let key2 = 1;;
Hello John!() : void
key2 = 1 : int
}
\noindent If a normal autoloading action is all that is required, the function
{autoload_theory} provides a simpler way.
\SEEALSO
autoload_theory, let_after, let_before, undo_autoload.
\ENDDOC
|