src/Tools/Graphview/tree_panel.scala
Tue, 27 Jun 2017 21:56:56 +0200 wenzelm clarified defaults;
Tue, 27 Jun 2017 21:36:58 +0200 wenzelm tuned signature;
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;
less more (0) -10 -7 tip