src/Tools/Graphview/metrics.scala
2015-01-18 wenzelm 2015-01-18 prefer fractional font metrics, for proper scaling of node size;
2015-01-18 wenzelm 2015-01-18 tuned metrics;
2015-01-17 wenzelm 2015-01-17 more explicit Layout.Info: size and content; allow multi-line vertex label, based on content; misc tuning;
2015-01-06 wenzelm 2015-01-06 explict layout graph structure, with dummies and coordinates; explicit metrics for dummy box; tuned signature; misc tuning;
2015-01-05 wenzelm 2015-01-05 tuned metrics;
2015-01-05 wenzelm 2015-01-05 separate module Metrics; maintain static metrics (with font) and visible_graph via layout;