src/Pure/Isar/token.ML
Sat, 01 Apr 2023 14:50:43 +0200 wenzelm clarified signature;
Mon, 06 Dec 2021 15:34:54 +0100 wenzelm discontinued old-style {* verbatim *} tokens;
Tue, 23 Nov 2021 16:06:09 +0100 wenzelm output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;
Thu, 21 Oct 2021 18:10:51 +0200 wenzelm clarified modules;
Wed, 20 Oct 2021 20:04:28 +0200 wenzelm clarified modules;
Wed, 20 Oct 2021 16:36:49 +0200 wenzelm clarified signature;
Tue, 28 Sep 2021 16:01:13 +0200 wenzelm outer syntax: support for control-cartouche tokens;
Mon, 23 Aug 2021 20:18:00 +0200 wenzelm minor performance tuning;
Mon, 23 Aug 2021 14:24:57 +0200 wenzelm clarified signature;
Mon, 23 Aug 2021 12:54:28 +0200 wenzelm clarified signature;
Fri, 14 May 2021 21:32:11 +0200 wenzelm reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
Fri, 03 Apr 2020 17:35:10 +0200 wenzelm less redundant markup reports;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Fri, 01 Mar 2019 16:49:41 +0100 wenzelm clarified signature;
Tue, 31 Jul 2018 21:21:20 +0200 wenzelm tuned signature;
Tue, 31 Jul 2018 21:11:24 +0200 wenzelm clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
Sun, 27 May 2018 13:42:01 +0200 wenzelm markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
Mon, 14 May 2018 22:01:00 +0200 wenzelm adjust position according to offset of command/exec id;
Sun, 18 Feb 2018 19:18:49 +0100 wenzelm clarified signature;
Thu, 25 Jan 2018 11:29:52 +0100 wenzelm clarified signature;
Thu, 25 Jan 2018 11:20:31 +0100 wenzelm tuned message;
Wed, 24 Jan 2018 20:47:36 +0100 wenzelm clarified operations;
Wed, 24 Jan 2018 20:08:33 +0100 wenzelm tuned signature: removed unused operations;
Wed, 24 Jan 2018 16:34:24 +0100 wenzelm clarified signature;
Wed, 24 Jan 2018 11:56:38 +0100 wenzelm clarified operations;
Tue, 16 Jan 2018 11:27:52 +0100 wenzelm discontinued old form of marginal comments;
Mon, 15 Jan 2018 23:03:01 +0100 wenzelm clarified markup;
Mon, 15 Jan 2018 22:46:04 +0100 wenzelm more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
Mon, 12 Jun 2017 11:32:23 +0200 wenzelm more markup for HTML rendering;
Mon, 12 Jun 2017 10:58:10 +0200 wenzelm tuned signature;
less more (0) -100 -50 -30 tip