| Wed, 31 Jan 2018 11:18:36 +0100 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Wed, 31 Jan 2018 11:09:05 +0100 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 30 Jan 2018 23:01:38 +0100 |
wenzelm |
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
|
changeset |
files
|
| Tue, 30 Jan 2018 22:46:00 +0100 |
wenzelm |
clarified lines: like split_lines;
|
changeset |
files
|
| Tue, 30 Jan 2018 20:36:18 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 30 Jan 2018 20:21:55 +0100 |
wenzelm |
unused;
|
changeset |
files
|
| Tue, 30 Jan 2018 20:20:46 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 30 Jan 2018 20:12:41 +0100 |
wenzelm |
simplified: prod_count is always NONE;
|
changeset |
files
|
| Tue, 30 Jan 2018 19:59:15 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 30 Jan 2018 19:45:08 +0100 |
wenzelm |
tuned data structure and operations;
|
changeset |
files
|
| Tue, 30 Jan 2018 18:38:18 +0100 |
wenzelm |
tuned data structure and operations;
|
changeset |
files
|
| Tue, 30 Jan 2018 16:12:50 +0100 |
wenzelm |
tuned data structure and operations;
|
changeset |
files
|
| Tue, 30 Jan 2018 16:05:33 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Tue, 30 Jan 2018 15:40:01 +0100 |
wenzelm |
prefer specific tokens_subtract: subtle change of comparison via tokens_match;
|
changeset |
files
|
| Tue, 30 Jan 2018 15:15:51 +0100 |
wenzelm |
tuned type: absorb NONE: token option as token_none: token;
|
changeset |
files
|
| Tue, 30 Jan 2018 14:31:33 +0100 |
wenzelm |
tuned;
|
changeset |
files
|