src/Pure/Isar/token.scala
Tue, 28 Sep 2021 16:01:13 +0200 wenzelm outer syntax: support for control-cartouche tokens;
Fri, 27 Nov 2020 16:40:31 +0100 wenzelm unused (see 7634d33c1a79);
Fri, 20 Nov 2020 23:47:34 +0100 wenzelm generate theory HTML in Isabelle/Scala;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Sun, 06 Jan 2019 12:42:26 +0100 wenzelm support for isabelle update -u path_cartouches;
Sun, 30 Dec 2018 16:56:31 +0100 wenzelm exclude file name components that are special on Windows;
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;
Sat, 17 Mar 2018 20:32:39 +0100 wenzelm more position information;
Tue, 16 Jan 2018 11:27:52 +0100 wenzelm discontinued old form of marginal comments;
Tue, 16 Jan 2018 09:08:06 +0100 wenzelm tuned signature;
Mon, 15 Jan 2018 22:46:04 +0100 wenzelm more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
Sun, 14 Jan 2018 19:45:48 +0100 wenzelm clarified Token.is_text (cf. Parse.text in ML);
Mon, 04 Dec 2017 22:56:46 +0100 wenzelm added action to make antiquoted cartouche;
Wed, 25 Oct 2017 11:40:58 +0200 wenzelm disallow blanks, relevant for session_name / theory_name e.g. in build log files;
Wed, 25 Oct 2017 11:35:48 +0200 wenzelm uniform system name;
Thu, 20 Apr 2017 14:59:57 +0200 wenzelm more operations;
Mon, 20 Mar 2017 20:43:26 +0100 wenzelm support to encode/decode command state;
Sat, 07 Jan 2017 20:01:05 +0100 wenzelm tuned signature;
Sat, 31 Dec 2016 21:00:43 +0100 wenzelm more precise markup;
Mon, 26 Dec 2016 13:21:08 +0100 wenzelm clarified header text;
Mon, 07 Nov 2016 19:09:10 +0100 wenzelm more uniform path syntax, as in ML (see 5a7c919a4ada);
Wed, 13 Jul 2016 19:04:49 +0200 wenzelm clarified indentation: 'begin' is treated like a separate command without indent;
Mon, 11 Jul 2016 20:37:28 +0200 wenzelm indentation of brackets;
Mon, 11 Jul 2016 18:18:24 +0200 wenzelm tunes signature;
Mon, 11 Jul 2016 16:36:29 +0200 wenzelm explicit kind "before_command";
Thu, 07 Jul 2016 21:34:56 +0200 wenzelm clarified signature;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Fri, 08 Jan 2016 17:17:43 +0100 wenzelm tuned;
less more (0) -50 -30 tip