Changes

Summary

1. clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
2. clarified lines: like split_lines;
3. tuned;
4. unused;
5. tuned;
6. simplified: prod_count is always NONE;
7. tuned;
8. tuned data structure and operations;
9. tuned data structure and operations;
10. tuned data structure and operations;
11. more operations;
12. prefer specific tokens_subtract: subtle change of comparison via tokens_match;
13. tuned type: absorb NONE: token option as token_none: token;
14. tuned;
15. clarified types and operations: potentially more efficient add_prods; tuned data structure;
16. clarified modules; tuned;
17. tuned: more explicit types;