src/Tools/Graphview/shapes.scala
2016-04-02 wenzelm 2016-04-02 more robust display of bidirectional Unicode text: enforce left-to-right;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-01-28 wenzelm 2015-01-28 clarified module name;
2015-01-19 wenzelm 2015-01-19 tuned colors;
2015-01-19 wenzelm 2015-01-19 clarified edge_color;
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 tuned signature;
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 clarified visualizer parameters; do not show dummies by default;
2015-01-05 wenzelm 2015-01-05 tuned metrics;
2015-01-05 wenzelm 2015-01-05 proper bounding box including dummies;
2015-01-05 wenzelm 2015-01-05 more direct coordinates for dummy;
2015-01-05 wenzelm 2015-01-05 separate module Metrics; maintain static metrics (with font) and visible_graph via layout;
2015-01-04 wenzelm 2015-01-04 explicit Layout.Point; tuned signature; tuned;
2015-01-04 wenzelm 2015-01-04 tuned signature;
2015-01-03 wenzelm 2015-01-03 tuned;
2015-01-03 wenzelm 2015-01-03 tuned;
2015-01-03 wenzelm 2015-01-03 tuned;
2015-01-03 wenzelm 2015-01-03 tuned signature;
2015-01-03 wenzelm 2015-01-03 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge; misc tuning; tuned signature;
2015-01-03 wenzelm 2015-01-03 prefer integer coordinates; tuned painting;
2015-01-03 wenzelm 2015-01-03 clarified bounding box, similar to old graph browser; default font like old browser; clarified metrics; tuned signature;
2015-01-02 wenzelm 2015-01-02 tuned headers;
2015-01-02 wenzelm 2015-01-02 clarified metrics, similar to old graph browser;
2015-01-01 wenzelm 2015-01-01 more dynamic visualizer -- re-use jEdit font info;
2015-01-01 wenzelm 2015-01-01 tuned signature;
2014-12-30 wenzelm 2014-12-30 clarified source location;