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
56
57
58
59
60
61
62
63
64
65
|
\DOC new_syntax_block
\TYPE {new_syntax_block : ((string # string # string) -> void)}
\SYNOPSIS
Declares a new syntax block.
\DESCRIBE
A syntax block starts with keyword and ends with a terminator and is
associated with a function of strings. When such a block is
encountered in the input stream, all the characters between the start
keyword and the terminator are made into a string to which the
associated function is applied.
The ML function {new_syntax_block} declares a new syntax block. The
first argument is the start keyword of the block, the second argument
is the terminator and the third argument is the name of a function
having a type which is an instance of {string->*}. The effect of
{
new_syntax_block(`XXX`, `YYY`, `Fun`);;
}
\noindent is that if
{
XXX
...
YYY
}
\noindent occurs in the input, then it is as though
{
Fun `
...
`
}
\noindent were input.
\FAILURE
Never fails.
\EXAMPLE
{
#let foo s = print_string `Hello: `; print_string s; print_newline();;
foo = - : (string -> void)
#new_syntax_block(`FOO`,`OOF`, `foo`);;
() : void
#FOO 123OO44OOF;;
Hello: 123OO44
() : void
#FOO
#splat
#OOF;;
Hello: splat
() : void
}
\USES
Interfacing parsers to HOL.
\ENDDOC
|
