| Tue, 11 Dec 2012 21:28:37 +0100 | wenzelm | more official graphics context with font metrics; | changeset | files |
| Tue, 11 Dec 2012 21:05:38 +0100 | wenzelm | just one class with parameters; | changeset | files |
| Tue, 11 Dec 2012 12:17:20 +0100 | wenzelm | initial layout coordinates more like old browser; | changeset | files |
| Tue, 11 Dec 2012 10:35:42 +0100 | wenzelm | added speculative options for jEdit; | changeset | files |
| Mon, 10 Dec 2012 21:55:57 +0100 | wenzelm | separate instance of class Parameters for each Main_Panel -- avoid global program state; | changeset | files |
| Mon, 10 Dec 2012 21:28:01 +0100 | wenzelm | discontinued long names flag -- better done via entity markup, without affecting layout; | changeset | files |
| Mon, 10 Dec 2012 20:52:57 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 10 Dec 2012 20:32:13 +0100 | wenzelm | tuned; | changeset | files |