src/Pure/ML/ml_heap.scala
Tue, 11 Jun 2024 21:32:26 +0200 wenzelm clarified signature: pro-forma support for Bytes with size: Long;
Tue, 16 Apr 2024 11:39:02 +0200 wenzelm tuned;
Tue, 16 Apr 2024 11:20:30 +0200 wenzelm tuned;
Tue, 16 Apr 2024 11:00:46 +0200 wenzelm more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
Thu, 11 Apr 2024 12:04:44 +0200 wenzelm tuned messages;
Sun, 10 Mar 2024 10:50:12 +0100 wenzelm tuned signature: more uniform SQL.Data instances;
Mon, 04 Mar 2024 21:22:22 +0100 wenzelm tuned messages;
Sat, 24 Feb 2024 16:30:25 +0100 wenzelm minor performance tuning: just 1 transaction for slices <= 1;
Sat, 24 Feb 2024 15:10:50 +0100 wenzelm tuned;
Thu, 22 Feb 2024 20:05:24 +0100 wenzelm minor performance tuning;
Thu, 22 Feb 2024 13:57:13 +0100 wenzelm clarified signature;
Thu, 22 Feb 2024 13:27:15 +0100 wenzelm more robust: make double-sure that heap digest is present;
Thu, 22 Feb 2024 13:24:26 +0100 wenzelm tuned;
Thu, 22 Feb 2024 13:19:36 +0100 wenzelm minor performance tuning: just one transaction for log_db without heap;
Thu, 22 Feb 2024 13:12:10 +0100 wenzelm tuned;
Thu, 22 Feb 2024 12:53:07 +0100 wenzelm clarified store_session: heap requires process_result.ok, but log_db is always stored;
Thu, 22 Feb 2024 12:22:13 +0100 wenzelm unused;
Thu, 22 Feb 2024 12:19:23 +0100 wenzelm tuned;
Thu, 22 Feb 2024 12:14:55 +0100 wenzelm tuned names;
Thu, 22 Feb 2024 11:52:29 +0100 wenzelm tuned names;
Wed, 21 Feb 2024 20:37:53 +0100 wenzelm clarified database layout;
Wed, 21 Feb 2024 20:21:30 +0100 wenzelm tuned signature;
Wed, 21 Feb 2024 19:54:17 +0100 wenzelm more accurate types;
Wed, 21 Feb 2024 19:36:53 +0100 wenzelm build local log_db, with store/restore via optional database server;
Mon, 19 Feb 2024 16:25:06 +0100 wenzelm tuned;
Mon, 19 Feb 2024 11:47:51 +0100 wenzelm clarified signature;
Mon, 19 Feb 2024 11:39:15 +0100 wenzelm clarified names;
Sun, 12 Nov 2023 12:34:04 +0100 wenzelm more robust: prefer strict operations;
Sun, 12 Nov 2023 12:26:08 +0100 wenzelm tuned signature: more operations;
Sat, 11 Nov 2023 22:14:38 +0100 wenzelm clarified signature;
less more (0) -50 -30 tip