File: inject_input.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (31 lines) | stat: -rw-r--r-- 620 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
31
 
\DOC inject_input

\TYPE {inject_input : (int list -> void)}

\SYNOPSIS
Passes a list of character codes to the ML interpreter.

\DESCRIBE
When applied to a list of character codes, {inject_input} passes these to the
ML interpreter, which will, after evaluating other pending phrases, interpret
them.

\FAILURE
The injection of input never fails, but of course the subsequent interpretation
may do.

\EXAMPLE
{
#inject_input (map ascii_code (explode `tty_write \`Yo!\`;;\
#`));;
() : void

Yo!() : void
}
\COMMENTS
The function {ML_eval} is similar, and easier to use.

\SEEALSO
let_after, let_before, ML_eval.

\ENDDOC