| Thu, 04 Apr 2024 11:40:45 +0200 |
wenzelm |
more portable: prefer official JDBC operation DatabaseMetaData.getColumns();
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 20:31:35 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2024 10:50:12 +0100 |
wenzelm |
tuned signature: more uniform SQL.Data instances;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2024 11:05:32 +0100 |
wenzelm |
tuned signature: prefer bottom-up construction;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2024 20:38:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2024 20:29:05 +0100 |
wenzelm |
more operations for Build_Log.Meta_Info: prefer explicit types;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2024 20:03:21 +0100 |
wenzelm |
more accurate patterns --- reverting unused fc3ba0a1c82f;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2024 19:18:39 +0100 |
wenzelm |
remove unused/fragile option (amending db37cae970a6) --- universal_table requires pull_date tables;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2024 18:29:21 +0100 |
wenzelm |
additional build_log column "session_start", with implicit upgrade of database schema;
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 20:47:33 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 20:41:18 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 20:18:44 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 20:09:20 +0100 |
wenzelm |
clarified modules: Build_Log.private_data provides raw data access without transaction_lock;
|
file |
diff |
annotate
|
| Sat, 25 Nov 2023 17:33:29 +0100 |
wenzelm |
more thorough transaction_lock;
|
file |
diff |
annotate
|
| Mon, 20 Nov 2023 14:23:11 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 20 Nov 2023 13:08:50 +0100 |
wenzelm |
clarified operation: pick current pull_date instead of previous one;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 15:15:09 +0100 |
wenzelm |
clarified signature: more operations and options concerning Isabelle hg;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 12:51:47 +0100 |
wenzelm |
unused (see also 004b39bf06a5);
|
file |
diff |
annotate
|
| Sun, 19 Nov 2023 12:46:41 +0100 |
wenzelm |
clarified signature and modules: more explicit Build_Log.History;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 16:58:14 +0100 |
wenzelm |
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2023 15:44:46 +0100 |
wenzelm |
proper ml_statistics (amending aeb511a520f4);
|
file |
diff |
annotate
|
| Wed, 08 Nov 2023 20:31:29 +0100 |
wenzelm |
proper default for disjunction (amending 9f7a94117666);
|
file |
diff |
annotate
|
| Sat, 04 Nov 2023 17:29:49 +0100 |
wenzelm |
clarified "recent" time: days <= 0 means infinity (no constraint);
|
file |
diff |
annotate
|
| Sat, 04 Nov 2023 16:07:22 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 14:31:01 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 13:16:06 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 13:05:29 +0100 |
wenzelm |
just one pass is sufficient (see also cc8391b92747, 3e8a897042d9);
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 12:03:30 +0100 |
wenzelm |
more detailed progress for build_log_database, to see better what happens when;
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 10:29:24 +0100 |
wenzelm |
more uniform progress;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 16:45:39 +0100 |
wenzelm |
proper Compress.Cache;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 16:24:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 16:15:59 +0100 |
wenzelm |
more parallelism via consumer thread: with mailbox limit to avoid ressource problems;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 14:35:51 +0100 |
wenzelm |
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2023 14:26:19 +0100 |
wenzelm |
clarified database transactions (see also 2c704ae04db1, 7bd0a250183b);
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 18:49:42 +0100 |
wenzelm |
performance tuning: more careful database access;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 11:57:01 +0100 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 11:49:33 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Oct 2023 11:39:17 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 22:44:31 +0200 |
wenzelm |
redundant (see also 3069da1743bc);
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 22:20:22 +0200 |
wenzelm |
removed obsolete table (see also 6acd1a2bd146);
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 22:10:22 +0200 |
wenzelm |
more robust init_database();
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 16:04:48 +0200 |
wenzelm |
proper private_data.transaction_lock;
|
file |
diff |
annotate
|
| Thu, 26 Oct 2023 15:38:27 +0200 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 20:12:07 +0200 |
Fabian Huch |
read relative cpu from build log;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 18:48:49 +0200 |
Fabian Huch |
defined statically known tables of Build_Log;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2023 21:11:59 +0200 |
wenzelm |
prefer Exn.result: avoid accidental capture of interrupts, similar to ML;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 21:54:35 +0200 |
wenzelm |
proper pattern (amending ff86f10e54cd);
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 17:17:12 +0200 |
wenzelm |
clarified signature: prefer enum types;
|
file |
diff |
annotate
|
| Tue, 29 Aug 2023 12:53:28 +0200 |
wenzelm |
misc tuning: support "scalac -source 3.3";
|
file |
diff |
annotate
|
| Tue, 18 Jul 2023 23:03:39 +0200 |
wenzelm |
more options for performance tuning;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2023 12:19:12 +0200 |
wenzelm |
clarified signature: eliminate SQL.Tables.empty to avoid confusion (see also 0bd366fad888);
|
file |
diff |
annotate
|
| Sun, 16 Jul 2023 09:50:42 +0200 |
wenzelm |
proper close() operation;
|
file |
diff |
annotate
|
| Sat, 15 Jul 2023 19:34:48 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Fri, 14 Jul 2023 14:56:48 +0200 |
wenzelm |
clarified signature: follow Store.open_database;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2023 13:13:10 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 21 Jun 2023 14:27:51 +0200 |
wenzelm |
clarified signature: more explicit class SQL.Data;
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 11:47:43 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2023 19:10:01 +0200 |
wenzelm |
proper stmt.execute() within loop (amending 9d9b30741fc4);
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 21:28:48 +0200 |
wenzelm |
more informative errors;
|
file |
diff |
annotate
|
| Wed, 29 Mar 2023 21:23:56 +0200 |
wenzelm |
clarified options;
|
file |
diff |
annotate
|