src/Pure/General/graph_display.scala
Sun, 25 Jan 2015 17:17:37 +0100 wenzelm tuned comments;
Sat, 03 Jan 2015 20:22:27 +0100 wenzelm more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
Sat, 03 Jan 2015 15:45:01 +0100 wenzelm more uniform support for graph display in ML/Scala;
less more (0) tip