NEWS
changeset 67413 2555713586c8
parent 67402 b71431a2051e
child 67419 866b1ad870ac
     1.1 --- a/NEWS	Fri Jan 12 20:19:59 2018 +0100
     1.2 +++ b/NEWS	Sat Jan 13 11:22:46 2018 +0100
     1.3 @@ -118,6 +118,11 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 +* Unused formal text within inner syntax may be marked as
     1.8 +\<^cancel>\<open>text\<close>. Thus it is ignored within the formal language, but
     1.9 +still printed in the document (with special markup). This is an official
    1.10 +way to "comment-out" some text.
    1.11 +
    1.12  * Embedded languages such as inner syntax and ML may contain formal
    1.13  comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
    1.14  syntax, antiquotations are interpreted wrt. the presentation context of