src/Tools/Graphview/tree_panel.scala
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