| Wed, 12 Jun 2024 21:40:13 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sat, 01 Jul 2023 16:32:46 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2023 15:16:17 +0100 |
wenzelm |
more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 16:11:05 +0100 |
wenzelm |
obsolete --- superseded by SHA1.Shasum operations;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 16:04:17 +0100 |
wenzelm |
clarified signature, using right-associative operation;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 15:53:58 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 15:50:49 +0100 |
wenzelm |
tuned --- implicit split;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 15:46:27 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 15:11:07 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 14:54:15 +0100 |
wenzelm |
proper Shasum.digest, to emulate old form from build_history database;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 10:58:07 +0100 |
wenzelm |
prefer explicit shasum;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2022 13:13:59 +0200 |
wenzelm |
clarified while-loops;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2022 22:40:34 +0200 |
wenzelm |
tuned: eliminted do-while for the sake of scala3;
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 17:00:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2022 12:15:25 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2022 12:02:56 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2022 20:25:52 +0100 |
wenzelm |
tuned -- follow sha1_digest in src/Tools/Setup/src/Build.java;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2020 21:39:55 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Apr 2020 19:07:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2018 14:59:42 +0100 |
wenzelm |
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 12:16:12 +0200 |
wenzelm |
discontinued unused / untested distinction of separate PIDE modules;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2016 14:55:43 +0100 |
wenzelm |
proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
|
file |
diff |
annotate
|
| Thu, 24 Mar 2016 13:08:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 10:38:46 +0200 |
wenzelm |
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 12:04:40 +0100 |
wenzelm |
prefer abstract datatype -- in accordance to ML version;
|
file |
diff |
annotate
|
| Thu, 14 Nov 2013 17:17:57 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 20:17:04 +0100 |
wenzelm |
explicit module UTF8;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2012 11:07:36 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2012 12:26:41 +0200 |
wenzelm |
maintain set of source digests, including relevant parts of session entry;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:29:25 +0200 |
wenzelm |
more explicit java.io.{File => JFile};
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 20:59:02 +0200 |
wenzelm |
more SHA1.digest operations;
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 21:29:53 +0100 |
wenzelm |
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:18:19 +0100 |
wenzelm |
explicit indication of modules for independent Scala library;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2011 12:56:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 20:21:24 +0100 |
wenzelm |
explicit type SHA1.digest;
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 23:23:29 +0200 |
wenzelm |
digesting strings according to SHA-1 -- Scala version;
|
file |
diff |
annotate
|