src/Pure/General/codepoint.scala
Mon, 04 Nov 2024 22:05:20 +0100 wenzelm clarified modules;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 03 Mar 2022 15:12:38 +0100 wenzelm tuned imports;
Mon, 01 Mar 2021 19:41:52 +0100 wenzelm tuned --- fewer warnings;
Thu, 11 Jun 2020 14:13:04 +0200 wenzelm proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;
Sun, 12 Mar 2017 14:23:38 +0100 wenzelm discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
Wed, 28 Dec 2016 17:10:09 +0100 wenzelm clarified modules;
Tue, 20 Dec 2016 16:08:02 +0100 wenzelm more systematic text length wrt. encoding;
Tue, 20 Dec 2016 10:44:36 +0100 wenzelm more systematic text length;
Tue, 20 Dec 2016 08:53:26 +0100 wenzelm clarified modules;
less more (0) tip