src/Tools/Graphview/graphview.scala
20 months ago wenzelm 2018-01-30 clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
2015-11-06 wenzelm 2015-11-06 tuned;
2015-09-14 wenzelm 2015-09-14 avoid hardwired colors; more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);
2015-01-28 wenzelm 2015-01-28 tuned signature;
2015-01-28 wenzelm 2015-01-28 tuned signature;
2015-01-28 wenzelm 2015-01-28 clarified module name;