src/Tools/Graphview/tree_panel.scala
Tue, 11 Aug 2015 22:01:11 +0200 wenzelm clarified tree row handling;
Wed, 05 Aug 2015 20:19:51 +0200 wenzelm tuned;
Wed, 05 Aug 2015 20:02:44 +0200 wenzelm tuned;
Wed, 20 May 2015 22:22:27 +0200 wenzelm cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;
Wed, 28 Jan 2015 19:15:13 +0100 wenzelm clarified module name;
Mon, 19 Jan 2015 21:15:30 +0100 wenzelm always swap panels, which leads to slightly better GUI layout;
Mon, 19 Jan 2015 20:39:01 +0100 wenzelm tuned;
Mon, 19 Jan 2015 16:31:04 +0100 wenzelm proper tooltips -- override action toolTip which is empty here;
Sun, 18 Jan 2015 23:07:00 +0100 wenzelm discontinued attempt at alphabetic_order -- selection via regex should be sufficient;
Sun, 18 Jan 2015 22:43:53 +0100 wenzelm proper selection of nodes via regular expression;
Sun, 18 Jan 2015 22:20:48 +0100 wenzelm suppress some controls that don't work yet;
Sun, 18 Jan 2015 21:35:54 +0100 wenzelm proper scrolling wrt. transform;
Sun, 18 Jan 2015 20:15:05 +0100 wenzelm clarified main actions and keyboard focus;
Sun, 18 Jan 2015 19:21:10 +0100 wenzelm tuned signature;
Sun, 18 Jan 2015 17:34:14 +0100 wenzelm support for tree view on graph nodes;
less more (0) tip