def text.spaces

ezsys@0.1.0.0 · src/str.bend:11

import Base

11# Python's whitespace (str.isspace, str.strip with no argument): the code
12# points 9 to 13, 28 to 32, 133, 160, 5760, 8192 to 8202, 8232, 8233, 8239,
13# 8287 and 12288
14def text.spaces() -> List<&2, U32>:
15  [9, 10, 11, 12, 13, 28, 29, 30, 31, 32, 133, 160, 5760, 8192, 8193, 8194,
16    8195, 8196, 8197, 8198, 8199, 8200, 8201, 8202, 8232, 8233, 8239, 8287,
17    12288]