| Thu, 04 Apr 2013 18:44:22 +0200 | wenzelm | more conventional synchronized access to Options_Variable -- avoid Swing_Thread getting in the way, which might be absent in some environments (e.g. SWT); | changeset | files |
| Thu, 04 Apr 2013 18:25:47 +0200 | wenzelm | added missing file; | changeset | files |
| Thu, 04 Apr 2013 18:20:00 +0200 | wenzelm | tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree; | changeset | files |