src/Pure/Thy/sessions.scala
Mon, 13 Mar 2023 13:43:25 +0100 wenzelm clarified signature: more explicit types;
Mon, 13 Mar 2023 10:51:10 +0100 wenzelm tuned signature;
Sat, 11 Mar 2023 16:11:26 +0100 wenzelm tuned signature;
Sat, 11 Mar 2023 12:41:53 +0100 wenzelm clarified session prefs (or "options" within the database);
Thu, 09 Mar 2023 12:55:00 +0100 wenzelm more robust transactions;
Tue, 07 Mar 2023 16:23:48 +0100 wenzelm clarified structure;
Tue, 07 Mar 2023 12:40:10 +0100 wenzelm clarified signature: proper abstract type;
Mon, 06 Mar 2023 21:12:47 +0100 wenzelm clarified signature: reduce boilerplate;
Mon, 06 Mar 2023 16:06:24 +0100 wenzelm tuned: prefer iterator.nextOption;
Mon, 06 Mar 2023 15:56:28 +0100 wenzelm tuned whitespace and braces;
Mon, 06 Mar 2023 15:48:04 +0100 wenzelm clarified signature: more uniform operations;
Mon, 06 Mar 2023 15:38:50 +0100 wenzelm tuned signature: reduce boilerplate;
Mon, 06 Mar 2023 15:12:37 +0100 wenzelm tuned signature;
Mon, 06 Mar 2023 10:58:36 +0100 wenzelm tuned signature;
Sun, 05 Mar 2023 16:36:18 +0100 wenzelm clarified signature: manage "verbose" flag via "progress";
Sun, 05 Mar 2023 15:19:53 +0100 wenzelm tuned;
Thu, 02 Mar 2023 11:36:10 +0100 wenzelm clarified modules;
Thu, 02 Mar 2023 11:25:50 +0100 wenzelm tuned;
Thu, 02 Mar 2023 11:11:55 +0100 wenzelm clarified modules;
Wed, 01 Mar 2023 13:52:11 +0100 wenzelm avoid premature Properties.uncompress: allow blob to be stored in another database;
Sun, 26 Feb 2023 20:19:01 +0100 wenzelm misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
Sat, 25 Feb 2023 14:33:19 +0100 wenzelm clarified signature: more robust operations;
Fri, 24 Feb 2023 20:40:50 +0100 wenzelm tuned;
Mon, 13 Feb 2023 10:17:30 +0100 wenzelm clarified modules;
Mon, 06 Feb 2023 16:29:19 +0100 wenzelm tuned signature;
Mon, 06 Feb 2023 16:04:17 +0100 wenzelm clarified signature, using right-associative operation;
Mon, 06 Feb 2023 15:46:27 +0100 wenzelm clarified signature;
Mon, 06 Feb 2023 14:54:15 +0100 wenzelm proper Shasum.digest, to emulate old form from build_history database;
Mon, 06 Feb 2023 12:58:45 +0100 wenzelm prefer explicit shasum;
Mon, 06 Feb 2023 10:58:07 +0100 wenzelm prefer explicit shasum;
less more (0) -300 -100 -50 -30 tip