src/Pure/General/graph.scala
17 months ago wenzelm 2017-11-07 backed out odd "bug fix" 671decd2e627;
17 months ago wenzelm 2017-11-05 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");
18 months ago wenzelm 2017-10-10 more operations;
2016-10-24 wenzelm 2016-10-24 discontinued unused / untested distinction of separate PIDE modules;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-01-04 wenzelm 2015-01-04 clarified static full_graph vs. dynamic visible_graph; tuned;
2015-01-03 wenzelm 2015-01-03 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge; misc tuning; tuned signature;
2014-12-31 wenzelm 2014-12-31 converse graph according to Graph_Display;
2014-04-02 wenzelm 2014-04-02 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;
2012-12-10 wenzelm 2012-12-10 stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
2012-12-10 wenzelm 2012-12-10 clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
2012-12-09 wenzelm 2012-12-09 added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
2012-09-25 wenzelm 2012-09-25 added graph encode/decode operations; tuned signature;
2012-08-02 wenzelm 2012-08-02 tuned;
2012-07-26 wenzelm 2012-07-26 tuned signature;
2012-07-19 wenzelm 2012-07-19 clarified topological ordering: preserve order of adjacency via reverse fold;
2012-07-19 wenzelm 2012-07-19 clarified signature;
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-02-25 wenzelm 2012-02-25 tuned comments;
2012-02-25 wenzelm 2012-02-25 standard Graph instances;
2012-02-25 wenzelm 2012-02-25 clarified signature -- avoid oddities of Iterable like Iterator.map; specific toString;
2012-02-24 wenzelm 2012-02-24 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;
2012-02-24 wenzelm 2012-02-24 tuned signature;
2012-02-23 wenzelm 2012-02-23 tuned -- avoid copy of empty value;
2012-02-23 wenzelm 2012-02-23 tuned;
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2012-02-23 wenzelm 2012-02-23 further graph operations from ML;
2012-02-23 wenzelm 2012-02-23 directed graphs (in Scala);