src/Pure/General/comment.ML
4 months ago wenzelm 2019-03-24 clarified spell-checking (see also 30233285270a);
4 months ago wenzelm 2019-03-24 clarified signature;
4 months ago wenzelm 2019-03-24 more markup for various text kinds, notably for nested formal comments;
4 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;
17 months ago wenzelm 2018-02-03 clarified signature;
17 months ago wenzelm 2018-02-03 more uniform treatment of formal comments within document source; more robust nesting;
18 months ago wenzelm 2018-01-25 more markup: disable spell-checker for raw latex;
18 months ago wenzelm 2018-01-14 allow LaTeX source as formal comment;
18 months ago wenzelm 2018-01-14 clarified signature;
18 months ago wenzelm 2018-01-14 clarified modules: uniform notion of formal comments;