File: ML_eval.doc

package info (click to toggle)
hol88 2.02.19940316-15
  • links: PTS
  • area: main
  • in suites: wheezy
  • size: 65,928 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,075; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (30 lines) | stat: -rw-r--r-- 565 bytes parent folder | download | duplicates (11) 
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
 
\DOC ML_eval

\TYPE {ML_eval : (string -> void)}

\SYNOPSIS
Passes a string to the ML interpreter.

\KEYWORDS
interpret.

\DESCRIBE
When applied to a string, {ML_eval} will pass it to the ML interpreter, which,
after evaluating other pending phrases, will interpret it as if it had been
typed at toplevel.

\FAILURE
The call itself never fails, but of course the subsequent interpretation may do.

\EXAMPLE
{
#ML_eval(`let greeting = \`Hi there!\` in tty_write greeting;;
#`);;
() : void

Hi there!() : void
}
\SEEALSO
inject_input, let_after, let_before.

\ENDDOC