src/Pure/General/bytes.scala
Tue, 11 Jun 2024 16:32:10 +0200 wenzelm clarified signature: discontinue somewhat misleading Bytes <: CharSequence;
Tue, 11 Jun 2024 16:02:33 +0200 wenzelm minor performance tuning;
Tue, 11 Jun 2024 15:49:39 +0200 wenzelm clarified signature: more accurate types;
Tue, 11 Jun 2024 14:18:19 +0200 wenzelm clarified signature;
Sun, 21 Jan 2024 14:05:14 +0100 wenzelm clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
Sun, 21 Jan 2024 13:18:05 +0100 wenzelm unused;
Sun, 12 Nov 2023 12:26:08 +0100 wenzelm tuned signature: more operations;
Sat, 11 Nov 2023 22:17:14 +0100 wenzelm proper check_file operation via File.space (amending 6ad3a412ed97 --- broken in Isabelle2023);
Sat, 11 Nov 2023 22:14:38 +0100 wenzelm clarified signature;
Sat, 28 Oct 2023 19:13:02 +0200 wenzelm prefer old-style import "=>";
Sun, 02 Jul 2023 19:05:59 +0200 wenzelm tuned: prefer Scala over Java;
Thu, 22 Jun 2023 14:51:37 +0200 wenzelm more operations;
Sun, 26 Mar 2023 19:51:35 +0200 wenzelm clarified signature;
Sun, 26 Mar 2023 19:36:00 +0200 wenzelm tuned signature;
Sun, 26 Mar 2023 19:31:05 +0200 wenzelm tuned output;
Sun, 26 Mar 2023 15:02:08 +0200 wenzelm tuned;
Sun, 26 Mar 2023 14:45:28 +0200 wenzelm tuned output;
Sun, 26 Mar 2023 14:36:47 +0200 wenzelm tuned performance: much faster low-level operation;
Sun, 26 Mar 2023 14:24:38 +0200 wenzelm clarified signature: more general operation Bytes.read_slice;
Sat, 22 Oct 2022 16:56:17 +0200 wenzelm tuned: avoid redundant copy of potentially large array;
Fri, 21 Oct 2022 21:39:38 +0200 wenzelm clarified signature;
Fri, 21 Oct 2022 18:06:32 +0200 wenzelm clarified signature;
Fri, 21 Oct 2022 16:39:31 +0200 wenzelm generic support for XZ and Zstd compression in Isabelle/Scala;
Fri, 21 Oct 2022 14:45:13 +0200 wenzelm clarified signature: default cache is actually dummy and not changed dynamically;
Sat, 01 Oct 2022 21:13:45 +0200 wenzelm clarified signature: more operations;
Wed, 27 Jul 2022 13:13:59 +0200 wenzelm clarified while-loops;
Sat, 25 Jun 2022 13:19:15 +0200 wenzelm clarified modules;
Wed, 22 Jun 2022 13:42:30 +0200 wenzelm clarified signature;
Wed, 22 Jun 2022 11:23:53 +0200 wenzelm tuned signature;
Wed, 22 Jun 2022 11:09:31 +0200 wenzelm clarified types and defaults;
less more (0) -50 -30 tip