+ Note that position 0 is still 0000, not 0020 as it might plausibly
+ be, because I didn't like the idea that converting several words
+ in Unicode through this table would produce NULs in place of all
+ the spaces! In principle that works fine, but it makes me uneasy.
+