src/Pure/General/scan.scala
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, 02 Jul 2023 19:05:59 +0200 wenzelm tuned: prefer Scala over Java;
Fri, 01 Apr 2022 23:19:12 +0200 wenzelm tuned formatting;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Mon, 07 Mar 2022 16:01:54 +0100 wenzelm more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Tue, 28 Sep 2021 16:01:13 +0200 wenzelm outer syntax: support for control-cartouche tokens;
Thu, 04 Mar 2021 21:04:27 +0100 wenzelm clarified signature --- fewer warnings;
Thu, 04 Mar 2021 15:59:28 +0100 wenzelm tuned --- fewer warnings;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Wed, 03 Mar 2021 22:31:11 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sat, 16 Jan 2021 22:52:43 +0100 wenzelm updated to scala-2.13.4;
Sun, 10 Jan 2021 13:04:29 +0100 wenzelm more informative errors: simplify diagnosis of spurious failures reported by users;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Wed, 15 Jan 2020 19:54:50 +0100 wenzelm misc tuning, following hint by IntelliJ;
Mon, 03 Dec 2018 14:59:42 +0100 wenzelm static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
Mon, 15 Jan 2018 14:31:57 +0100 wenzelm clarified modules;
Sun, 07 Jan 2018 21:04:51 +0100 wenzelm support for formal comments in ML in Isabelle/Scala;
Sun, 07 Jan 2018 20:44:48 +0100 wenzelm tuned;
Thu, 26 Oct 2017 23:31:03 +0200 wenzelm separate JSON lexer;
Wed, 25 Oct 2017 14:39:22 +0200 wenzelm more robust treatment of UTF8 in raw byte sources;
Sat, 07 Jan 2017 20:01:05 +0100 wenzelm tuned signature;
Tue, 02 Aug 2016 17:35:18 +0200 wenzelm support 'abbrevs' within theory header;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Thu, 08 Jan 2015 20:56:39 +0100 wenzelm tuned;
Mon, 01 Dec 2014 15:21:49 +0100 wenzelm more merge operations;
Wed, 01 Oct 2014 21:00:49 +0200 wenzelm actually finish after closing, e.g. relevant for consecutive (**)(**);
Fri, 02 May 2014 18:54:47 +0200 wenzelm avoid deprecated Scala syntax;
Fri, 02 May 2014 12:27:40 +0200 wenzelm support URLs as well;
less more (0) -50 -30 tip