src/Tools/Graphview/graph_file.scala
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;
2015-01-25 wenzelm 2015-01-25 support for off-line graph output, without GUI thread;
2015-01-25 wenzelm 2015-01-25 separate module Graph_File;