clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;

tuned;

avoid hardwired colors;
more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);

tuned signature;

tuned signature;

clarified module name;

--HG--
rename : src/Tools/Graphview/visualizer.scala => src/Tools/Graphview/graphview.scala