#
71da0b67 |
|
25-Jun-2018 |
wenzelm <none@none> |
more scalable output;
|
#
6284dfda |
|
29-May-2018 |
wenzelm <none@none> |
tuned signature;
|
#
2ae06ed1 |
|
23-Mar-2018 |
wenzelm <none@none> |
clarified signature;
|
#
ea1a4ba8 |
|
07-Nov-2017 |
wenzelm <none@none> |
backed out odd "bug fix" 671decd2e627;
|
#
ab100203 |
|
05-Nov-2017 |
wenzelm <none@none> |
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");
|
#
5a1a4eeb |
|
10-Oct-2017 |
wenzelm <none@none> |
more operations;
|
#
3ee6c0a8 |
|
23-Oct-2016 |
wenzelm <none@none> |
discontinued unused / untested distinction of separate PIDE modules;
|
#
a838e0a4 |
|
04-Jan-2015 |
wenzelm <none@none> |
clarified static full_graph vs. dynamic visible_graph; tuned;
|
#
331be8f5 |
|
03-Jan-2015 |
wenzelm <none@none> |
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge; misc tuning; tuned signature;
|
#
9848944b |
|
31-Dec-2014 |
wenzelm <none@none> |
converse graph according to Graph_Display;
|
#
e0e8cf48 |
|
02-May-2015 |
wenzelm <none@none> |
misc tuning, based on warnings by IntelliJ IDEA;
|
#
4f51da4c |
|
02-Apr-2014 |
wenzelm <none@none> |
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;
|
#
6e4b0730 |
|
10-Dec-2012 |
wenzelm <none@none> |
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
|
#
d309e32a |
|
10-Dec-2012 |
wenzelm <none@none> |
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
|
#
61ebd09b |
|
09-Dec-2012 |
wenzelm <none@none> |
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
|
#
231425cc |
|
25-Sep-2012 |
wenzelm <none@none> |
added graph encode/decode operations; tuned signature;
|
#
4b559c19 |
|
02-Aug-2012 |
wenzelm <none@none> |
tuned;
|
#
d1ab92f7 |
|
26-Jul-2012 |
wenzelm <none@none> |
tuned signature;
|
#
1c41f318 |
|
19-Jul-2012 |
wenzelm <none@none> |
clarified topological ordering: preserve order of adjacency via reverse fold;
|
#
86e2179a |
|
19-Jul-2012 |
wenzelm <none@none> |
clarified signature;
|
#
78b39fdb |
|
27-Feb-2012 |
wenzelm <none@none> |
prefer final ADTs -- prevent ooddities;
|
#
f4c54033 |
|
25-Feb-2012 |
wenzelm <none@none> |
tuned comments;
|
#
7001e39a |
|
25-Feb-2012 |
wenzelm <none@none> |
standard Graph instances;
|
#
7e41514d |
|
25-Feb-2012 |
wenzelm <none@none> |
clarified signature -- avoid oddities of Iterable like Iterator.map; specific toString;
|
#
8cc87c04 |
|
24-Feb-2012 |
wenzelm <none@none> |
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;
|
#
28ababb4 |
|
24-Feb-2012 |
wenzelm <none@none> |
tuned signature;
|
#
3eb6b91a |
|
23-Feb-2012 |
wenzelm <none@none> |
tuned -- avoid copy of empty value;
|
#
cae155a5 |
|
23-Feb-2012 |
wenzelm <none@none> |
tuned;
|
#
9f564a6a |
|
23-Feb-2012 |
wenzelm <none@none> |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
#
98ca5cf3 |
|
23-Feb-2012 |
wenzelm <none@none> |
further graph operations from ML;
|
#
0dd725d9 |
|
23-Feb-2012 |
wenzelm <none@none> |
directed graphs (in Scala);
|