src/Pure/General/comment.ML
8 weeks ago wenzelm 2019-03-24 clarified spell-checking (see also 30233285270a);
8 weeks ago wenzelm 2019-03-24 clarified signature;
8 weeks ago wenzelm 2019-03-24 more markup for various text kinds, notably for nested formal comments;
2 months ago wenzelm 2019-03-10 document markers are formal comments, and may thus occur anywhere in the command-span; clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure; tuned signature;
15 months ago wenzelm 2018-02-03 clarified signature;
15 months ago wenzelm 2018-02-03 more uniform treatment of formal comments within document source; more robust nesting;
16 months ago wenzelm 2018-01-25 more markup: disable spell-checker for raw latex;
16 months ago wenzelm 2018-01-14 allow LaTeX source as formal comment;
16 months ago wenzelm 2018-01-14 clarified signature;
16 months ago wenzelm 2018-01-14 clarified modules: uniform notion of formal comments;