src/Pure/PIDE/resources.scala
Fri, 05 Aug 2022 18:45:49 +0200 wenzelm clarified signature: more operations;
Thu, 04 Aug 2022 12:43:33 +0200 wenzelm clarified signature;
Thu, 04 Aug 2022 12:00:58 +0200 wenzelm clarified signature: proper session_name for Sessions.Base (like Sessions.Info);
Wed, 03 Aug 2022 12:25:37 +0200 wenzelm avoid multiple load_commands;
Wed, 22 Jun 2022 11:09:31 +0200 wenzelm clarified types and defaults;
Mon, 04 Apr 2022 23:46:14 +0200 wenzelm clarified signature: avoid ambiguity in scala3;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 11 Nov 2021 22:06:18 +0100 wenzelm clarified signature: prefer static operations;
Thu, 11 Nov 2021 21:54:28 +0100 wenzelm clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
Fri, 05 Nov 2021 12:05:17 +0100 wenzelm unused (see also 217e6cf61453, 5e7916535860);
Wed, 03 Nov 2021 14:26:13 +0100 wenzelm more PIDE markup;
Mon, 12 Apr 2021 18:10:13 +0200 wenzelm clarified signature for Scala functions;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sun, 20 Dec 2020 15:47:54 +0100 wenzelm present auxiliary files with PIDE markup;
less more (0) -100 -15 tip