src/Tools/Graphview/tree_panel.scala
24 months ago wenzelm 2017-06-27 clarified defaults;
24 months ago wenzelm 2017-06-27 tuned signature;
2015-08-11 wenzelm 2015-08-11 clarified tree row handling;
2015-08-05 wenzelm 2015-08-05 tuned;
2015-08-05 wenzelm 2015-08-05 tuned;
2015-05-20 wenzelm 2015-05-20 cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;
2015-01-28 wenzelm 2015-01-28 clarified module name;
2015-01-19 wenzelm 2015-01-19 always swap panels, which leads to slightly better GUI layout;
2015-01-19 wenzelm 2015-01-19 tuned;
2015-01-19 wenzelm 2015-01-19 proper tooltips -- override action toolTip which is empty here;
2015-01-18 wenzelm 2015-01-18 discontinued attempt at alphabetic_order -- selection via regex should be sufficient;
2015-01-18 wenzelm 2015-01-18 proper selection of nodes via regular expression;
2015-01-18 wenzelm 2015-01-18 suppress some controls that don't work yet;
2015-01-18 wenzelm 2015-01-18 proper scrolling wrt. transform; tuned signature;
2015-01-18 wenzelm 2015-01-18 clarified main actions and keyboard focus;
2015-01-18 wenzelm 2015-01-18 tuned signature;
2015-01-18 wenzelm 2015-01-18 support for tree view on graph nodes; misc tuning;