src/Pure/General/comment.ML
Thu, 02 May 2019 14:05:59 +0200 wenzelm clarified PIDE markup;
Sun, 24 Mar 2019 17:53:46 +0100 wenzelm clarified spell-checking (see also 30233285270a);
Sun, 24 Mar 2019 17:33:11 +0100 wenzelm clarified signature;
Sun, 24 Mar 2019 17:24:24 +0100 wenzelm more markup for various text kinds, notably for nested formal comments;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Sat, 03 Feb 2018 20:46:28 +0100 wenzelm clarified signature;
Sat, 03 Feb 2018 20:34:26 +0100 wenzelm more uniform treatment of formal comments within document source;
Thu, 25 Jan 2018 15:21:05 +0100 wenzelm more markup: disable spell-checker for raw latex;
Sun, 14 Jan 2018 16:21:29 +0100 wenzelm allow LaTeX source as formal comment;
Sun, 14 Jan 2018 15:06:27 +0100 wenzelm clarified signature;
Sun, 14 Jan 2018 14:11:02 +0100 wenzelm clarified modules: uniform notion of formal comments;
less more (0) tip