src/Pure/Admin/afp.scala
Sun, 13 Oct 2019 16:36:41 +0200 wenzelm tuned signature;
Wed, 10 Apr 2019 12:11:30 +0200 wenzelm tuned;
Wed, 27 Mar 2019 12:08:08 +0100 wenzelm more operations;
Mon, 25 Mar 2019 19:50:52 +0100 wenzelm RDF meta data for AFP entries;
Mon, 25 Mar 2019 17:21:26 +0100 wenzelm more strict AFP properties;
Mon, 25 Mar 2019 16:45:08 +0100 wenzelm tuned signature;
Mon, 25 Mar 2019 16:11:28 +0100 wenzelm clarified signature;
Mon, 25 Mar 2019 15:48:08 +0100 wenzelm proper treatment of empty extra lines (amending 98a440cfbb2b);
Mon, 25 Mar 2019 15:38:56 +0100 wenzelm clarified signature: explicitly typed interfaces;
Mon, 25 Mar 2019 14:47:54 +0100 wenzelm provide maintainers as seen in AFP/admin;
Mon, 25 Mar 2019 14:40:28 +0100 wenzelm tuned;
Mon, 25 Mar 2019 14:32:33 +0100 wenzelm tuned signature;
Mon, 25 Mar 2019 14:19:26 +0100 wenzelm read AFP metadata for entries;
Mon, 04 Feb 2019 14:03:31 +0100 wenzelm clarified URL -- avoid odd certificate problem with api.media.atlassian.com;
Sat, 19 Jan 2019 20:18:26 +0100 wenzelm more official AFP.groups;
Sun, 11 Mar 2018 13:18:41 +0100 wenzelm clarified AFP partitioning;
Sat, 10 Mar 2018 20:24:00 +0100 wenzelm more balanced AFP partitioning;
Thu, 08 Mar 2018 11:20:45 +0100 wenzelm more balanced AFP partitioning;
Tue, 06 Mar 2018 17:44:19 +0100 wenzelm more balanced AFP partitioning;
Sun, 12 Nov 2017 12:41:05 +0100 wenzelm tuned signature;
Tue, 07 Nov 2017 16:50:26 +0100 wenzelm tuned signature;
Tue, 07 Nov 2017 16:44:25 +0100 wenzelm clarifified selection: always wrt. build_graph structure;
Sat, 14 Oct 2017 16:59:45 +0200 wenzelm partition AFP sessions according to structure, which happens to cut it roughly into equal parts;
Fri, 13 Oct 2017 13:31:56 +0200 wenzelm tuned;
Thu, 12 Oct 2017 21:22:02 +0200 wenzelm entries_graph requires acyclic graph, but lazy val allows forming the AFP object nonetheless;
Tue, 10 Oct 2017 19:48:29 +0200 wenzelm cycle check with informative error;
Tue, 10 Oct 2017 19:23:03 +0200 wenzelm tuned: each session has at most one defining entry;
Mon, 09 Oct 2017 22:03:05 +0200 wenzelm tuned: less oo-non-sense;
Mon, 09 Oct 2017 21:43:27 +0200 wenzelm operations for graph display;
Mon, 09 Oct 2017 20:26:02 +0200 wenzelm dependencies of entries vs. sessions;
Mon, 09 Oct 2017 17:09:08 +0200 wenzelm some administrative support for AFP;
less more (0) tip