src/Pure/General/comment.ML
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