File: maptok.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 (32 lines) | stat: -rw-r--r-- 916 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
32
\DOC maptok

\TYPE {maptok : ((string -> *) -> string -> * list)}

\SYNOPSIS
Maps a function over the constituent words of a string.

\DESCRIBE
{maptok f s} first splits the string {s} into a list of substrings, and then
maps the function {f} over that list. Splitting of the string occurs at each
sequence of blanks and carriage returns (white space). This white space does
not appear in the list of substrings. Leading and trailing white space in the
input string is also thrown away.

\FAILURE
Fails if one of the applications of {f} to a substring fails.

\EXAMPLE
{
#maptok explode `  the cat  sat `;;
[[`t`; `h`; `e`]; [`c`; `a`; `t`]; [`s`; `a`; `t`]] : string list list
}
\USES
Useful when wanting to map a function over a list of constant strings.
Instead of using {map f [`string1`;...;`stringn`]} one can use:
{
   (maptok f `string1 ... stringn`)
}
\SEEALSO
words, word_separators, words2, map.

\ENDDOC