| Sun, 10 Nov 2024 12:15:31 +0100 | wenzelm | clarified margin operations (again, reverting 4794576828df); | file | diff | annotate |
| Sat, 09 Nov 2024 16:34:14 +0100 | wenzelm | clarified signature: include standard margin in object equality; | file | diff | annotate |
| Fri, 08 Nov 2024 15:08:36 +0100 | wenzelm | more accurate pretty_margin for proportional fonts; | file | diff | annotate |
| Fri, 08 Nov 2024 14:44:29 +0100 | wenzelm | clarified signature: more uniform; | file | diff | annotate |
| Wed, 06 Nov 2024 15:17:39 +0100 | wenzelm | more robust and uniform metric, still with special treatment motivated by jEdit (see also 0cdfce0bf956); | file | diff | annotate |
| Mon, 04 Nov 2024 21:54:34 +0100 | wenzelm | support value-oriented Font_Metric, e.g. for caching Pretty output; | file | diff | annotate |
| Mon, 04 Nov 2024 21:25:26 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 04 Nov 2024 21:05:05 +0100 | wenzelm | tuned; | file | diff | annotate |
| Mon, 04 Nov 2024 20:55:01 +0100 | wenzelm | clarified signature; | file | diff | annotate |