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;
less more (0) -7 tip