more scalable output;

tuned signature;

clarified signature;

backed out odd "bug fix" 671decd2e627;

uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");

more operations;

discontinued unused / untested distinction of separate PIDE modules;

clarified static full_graph vs. dynamic visible_graph;
tuned;

more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
misc tuning;
tuned signature;

converse graph according to Graph_Display;

misc tuning, based on warnings by IntelliJ IDEA;

more explicit iterator terminology, in accordance to Scala 2.8 library;
clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics;
tuned output;

stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;

clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;

added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;

added graph encode/decode operations;
tuned signature;

tuned;

tuned signature;

clarified topological ordering: preserve order of adjacency via reverse fold;

clarified signature;

prefer final ADTs -- prevent ooddities;

tuned comments;

standard Graph instances;

clarified signature -- avoid oddities of Iterable like Iterator.map;
specific toString;

prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty;
discontinued map_nodes, del_nodes conveniences -- avoid inefficient mapValues wrapper (this is not Table.map from ML);
tuned signature;

tuned signature;

tuned -- avoid copy of empty value;

tuned;

clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;

further graph operations from ML;

directed graphs (in Scala);