src/Pure/General/graph.scala
Sat, 01 Jul 2023 16:27:34 +0200 wenzelm clarified signature: proper equals/hashCode;
Sat, 31 Dec 2022 11:48:32 +0100 wenzelm clarified signature;
Fri, 01 Apr 2022 23:19:12 +0200 wenzelm tuned formatting;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 04 Mar 2021 15:49:15 +0100 wenzelm tuned --- fewer warnings;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Thu, 23 Jul 2020 14:25:48 +0200 wenzelm clarified order --- proper sorting of requirements;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Mon, 07 Oct 2019 17:20:26 +0200 wenzelm count document nodes via raw file length;
Mon, 07 Oct 2019 10:44:59 +0200 wenzelm clarified signature;
Mon, 30 Sep 2019 16:40:35 +0200 wenzelm support headless_load_limit for more scalable load process;
Sun, 29 Sep 2019 12:26:43 +0200 wenzelm more operations -- incremental exploration of reachable nodes;
Sun, 15 Sep 2019 13:42:01 +0200 wenzelm tuned signature;
Thu, 12 Sep 2019 16:52:04 +0200 wenzelm clarified signature: eliminated unused option;
Wed, 04 Sep 2019 20:05:57 +0200 wenzelm tuned messages;
Sun, 01 Sep 2019 22:57:25 +0200 wenzelm clarified signature: full dependency graph;
Mon, 25 Jun 2018 17:18:55 +0200 wenzelm more scalable output;
Tue, 29 May 2018 20:00:10 +0200 wenzelm tuned signature;
Fri, 23 Mar 2018 21:56:22 +0100 wenzelm clarified signature;
Tue, 07 Nov 2017 11:11:37 +0100 wenzelm backed out odd "bug fix" 671decd2e627;
Sun, 05 Nov 2017 16:57:03 +0100 wenzelm 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");
Tue, 10 Oct 2017 13:46:12 +0200 wenzelm more operations;
Mon, 24 Oct 2016 12:16:12 +0200 wenzelm discontinued unused / untested distinction of separate PIDE modules;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Sun, 04 Jan 2015 14:05:24 +0100 wenzelm clarified static full_graph vs. dynamic visible_graph;
Sat, 03 Jan 2015 20:22:27 +0100 wenzelm more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
Wed, 31 Dec 2014 21:45:30 +0100 wenzelm converse graph according to Graph_Display;
Wed, 02 Apr 2014 20:22:12 +0200 wenzelm more explicit iterator terminology, in accordance to Scala 2.8 library;
Mon, 10 Dec 2012 15:17:47 +0100 wenzelm stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
Mon, 10 Dec 2012 10:41:29 +0100 wenzelm clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
less more (0) -30 tip