| Mon, 08 Oct 2012 14:10:38 +0200 | wenzelm | prefer synchronous Mutator_Event.Bus on Swing_Thread; | changeset | files |
| Mon, 08 Oct 2012 13:20:55 +0200 | wenzelm | more direct tooltip content; | changeset | files |
| Mon, 08 Oct 2012 12:54:00 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 08 Oct 2012 12:40:35 +0200 | wenzelm | use Pretty_Tooltip for Graphview_Panel; | changeset | files |